X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=8932d21a86eec829cc62fb0f32dd38bd4bcc7a33;hb=6f7dbdfa37be6a1135df8169557eab5c92c485e2;hp=7fe26ff59c896b6abad5cd87bdf85c937b3ff94f;hpb=a3052afa2decd057bad64e5884eaa44b5e43ecdd;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 7fe26ff59..8932d21a8 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000-2003, HELM Team.
+(* Copyright (C) 2000-2004, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
@@ -53,16 +53,6 @@ let mqi_handle = MQIC.init mqi_flags prerr_string
let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
-let htmlheader =
- "" ^
- " "
-;;
-
-let htmlfooter =
- " " ^
- ""
-;;
-
let prooffile =
try
Sys.getenv "GTOPLEVEL_PROOFFILE"
@@ -89,8 +79,6 @@ let notify_hbugs_on_goal_change = false ;;
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
-let htmlheader_and_content = ref htmlheader;;
-
let check_term = ref (fun _ _ _ -> assert false);;
exception RenderingWindowsNotInitialized;;
@@ -121,11 +109,11 @@ exception OutputHtmlNotInitialized;;
let set_outputhtml,outputhtml =
let outputhtml_ref = ref None in
- (function rw -> outputhtml_ref := Some rw),
+ (function (rw: Ui_logger.html_logger) -> outputhtml_ref := Some rw),
(function () ->
match !outputhtml_ref with
- None -> raise OutputHtmlNotInitialized
- | Some outputhtml -> outputhtml
+ | None -> raise OutputHtmlNotInitialized
+ | Some outputhtml -> (outputhtml: Ui_logger.html_logger)
)
;;
@@ -179,17 +167,14 @@ let string_of_cic_textual_parser_uri uri =
String.sub uri' 4 (String.length uri' - 4)
;;
-let output_html outputhtml msg =
- htmlheader_and_content := !htmlheader_and_content ^ msg ;
- outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
- outputhtml#set_topline (-1)
-;;
+let output_html ?(append_NL = true) (outputhtml: Ui_logger.html_logger) =
+ outputhtml#log ~append_NL
(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
(* Check window *)
-let check_window outputhtml uris =
+let check_window (outputhtml: Ui_logger.html_logger) uris =
let window =
GWindow.window
~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
@@ -220,8 +205,7 @@ let check_window outputhtml uris =
mmlwidget#load_sequent [] (111,[],expr)
with
e ->
- output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
")
+ output_html outputhtml (`Error (`T (Printexc.to_string e)))
)
) uris
in
@@ -234,7 +218,7 @@ let check_window outputhtml uris =
exception NoChoice;;
let
- interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
+ interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok")
?(enable_button_for_non_vars=false) ~title ~msg uris
=
let choices = ref [] in
@@ -507,16 +491,14 @@ let qed () =
(** save an unfinished proof on the filesystem *)
let save_unfinished_proof () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
Xml.pp ~quiet:true xml (Some prooffiletype) ;
output_html outputhtml
- ("Current proof type saved to " ^
- prooffiletype ^ "
") ;
+ (`Msg (`T ("Current proof type saved to " ^ prooffiletype))) ;
Xml.pp ~quiet:true bodyxml (Some prooffile) ;
output_html outputhtml
- ("Current proof body saved to " ^
- prooffile ^ "
")
+ (`Msg (`T ("Current proof body saved to " ^ prooffile)))
;;
(* Used to typecheck the loaded proofs *)
@@ -541,7 +523,7 @@ let decompose_uris_choice_callback uris =
CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
| _ -> assert false)
(interactive_user_uri_choice
- ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false
+ ~selection_mode:`MULTIPLE ~ok:"Ok" ~enable_button_for_non_vars:false
~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
(List.map
(function (uri,typeno,_) ->
@@ -593,6 +575,10 @@ let refresh_proof (output : TermViewer.proof_viewer) =
prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
raise (InvokeTactics.RefreshProofException e)
+let set_proof_engine_goal g =
+ ProofEngine.goal := g
+;;
+
let refresh_goals ?(empty_notebook=true) notebook =
try
match !ProofEngine.goal with
@@ -672,7 +658,7 @@ module InvokeTacticsCallbacks =
end
;;
module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
-
+(*
(* Just to initialize the Hbugs module *)
module Ignore = Hbugs.Initialize (InvokeTactics');;
Hbugs.set_describe_hint_callback (fun hint ->
@@ -682,12 +668,12 @@ Hbugs.set_describe_hint_callback (fun hint ->
check_window outputhtml [term]
| _ -> ())
;;
-
+*)
let dummy_uri = "/dummy.con"
(** load an unfinished proof from filesystem *)
let load_unfinished_proof () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
try
@@ -701,40 +687,39 @@ let load_unfinished_proof () =
match CicParser.obj_of_xml prooffiletype (Some prooffile) with
Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
- ProofEngine.set_proof
- (Some (uri, metasenv, bo, ty)) ;
- ProofEngine.goal :=
+ ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ refresh_proof output ;
+ set_proof_engine_goal
(match metasenv with
[] -> None
| (metano,_,_)::_ -> Some metano
) ;
- refresh_proof output ;
refresh_goals notebook ;
output_html outputhtml
- ("Current proof type loaded from " ^
- prooffiletype ^ "
") ;
+ (`Msg (`T ("Current proof type loaded from " ^
+ prooffiletype))) ;
output_html outputhtml
- ("Current proof body loaded from " ^
- prooffile ^ "
") ;
+ (`Msg (`T ("Current proof body loaded from " ^
+ prooffile))) ;
!save_set_sensitive true;
| _ -> assert false
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let edit_aliases () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let id_to_uris = inputt#id_to_uris in
+ let id_to_uris = inputt#environment in
let chosen = ref false in
let window =
GWindow.window
@@ -744,7 +729,7 @@ let edit_aliases () =
let scrolled_window =
GBin.scrolled_window ~border_width:10
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
- let input = GEdit.text ~editable:true ~width:400 ~height:100
+ let input = GText.view ~editable:true ~width:400 ~height:100
~packing:scrolled_window#add () in
let hbox =
GPack.hbox ~border_width:0
@@ -759,65 +744,14 @@ let edit_aliases () =
ignore (cancelb#connect#clicked window#destroy) ;
ignore
(okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
- let dom,resolve_id = !id_to_uris in
ignore
- (input#insert_text ~pos:0
- (String.concat "\n"
- (List.map
- (function v ->
- let uri =
- match resolve_id v with
- None -> assert false
- | Some (CicTextualParser0.Uri uri) -> uri
- | Some (CicTextualParser0.Term _)
- | Some CicTextualParser0.Implicit -> assert false
- in
- "alias " ^
- (match v with
- CicTextualParser0.Id id -> id
- | CicTextualParser0.Symbol (descr,_) ->
- (* CSC: To be implemented *)
- assert false
- )^ " " ^ (string_of_cic_textual_parser_uri uri)
- ) dom))) ;
+ (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
+ (DisambiguatingParser.EnvironmentP3.to_string !id_to_uris)) ;
window#show () ;
GtkThread.main ();
if !chosen then
- let dom,resolve_id =
- let inputtext = input#get_chars 0 input#length in
- let regexpr =
- let alfa = "[a-zA-Z_-]" in
- let digit = "[0-9]" in
- let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
- let blanks = "\( \|\t\|\n\)+" in
- let nonblanks = "[^ \t\n]+" in
- let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
- Str.regexp
- ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
- in
- let rec aux n =
- try
- let n' = Str.search_forward regexpr inputtext n in
- let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in
- let uri =
- MQueryMisc.cic_textual_parser_uri_of_string
- ("cic:" ^ (Str.matched_group 5 inputtext))
- in
- let dom,resolve_id = aux (n' + 1) in
- if List.mem id dom then
- dom,resolve_id
- else
- id::dom,
- (function id' ->
- if id = id' then
- Some (CicTextualParser0.Uri uri)
- else resolve_id id')
- with
- Not_found -> TermEditor.empty_id_to_uris
- in
- aux 0
- in
- id_to_uris := (dom,resolve_id)
+ id_to_uris :=
+ DisambiguatingParser.EnvironmentP3.of_string (input#buffer#get_text ())
;;
let proveit () =
@@ -825,7 +759,7 @@ let proveit () =
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
let output = (rendering_window ())#output in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml (*: GHtml.xmhtml*)) in
try
output#make_sequent_of_selected_term ;
refresh_proof output ;
@@ -833,22 +767,22 @@ let proveit () =
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
")
+ (`Error (`T (Printexc.to_string e)))
;;
let focus () =
let module L = LogicalOperations in
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = (rendering_window ())#output in
try
output#focus_sequent_of_selected_term ;
@@ -856,15 +790,15 @@ let focus () =
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
")
+ (`Error (`T (Printexc.to_string e)))
;;
exception NoPrevGoal;;
@@ -874,7 +808,8 @@ let setgoal metano =
let module L = LogicalOperations in
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let output = (rendering_window ())#output in
+ let outputhtml = (rendering_window ())#outputhtml in
let metasenv =
match ProofEngine.get_proof () with
None -> assert false
@@ -885,11 +820,11 @@ let setgoal metano =
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
")
+ (`Error (`T (Printexc.to_string e)))
;;
let
@@ -906,7 +841,7 @@ let
let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
let href = Gdome.domString "href" in
let show_in_show_window_obj uri obj =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
let
(acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
@@ -915,7 +850,7 @@ let
Cic2acic.acic_object_of_cic_object obj
in
let mml =
- ApplyStylesheets.mml_of_cic_object
+ ChosenTransformer.mml_of_cic_object
~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types
in
window#set_title (UriManager.string_of_uri uri) ;
@@ -924,7 +859,7 @@ let
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
in
let show_in_show_window_uri uri =
let obj = CicEnvironment.get_obj uri in
@@ -967,7 +902,7 @@ let user_uri_choice ~title ~msg uris =
;;
let locate_callback id =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let out = output_html outputhtml in
let query = MQG.locate id in
let result = MQI.execute mqi_handle query in
@@ -976,10 +911,10 @@ let locate_callback id =
(function uri,_ ->
MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
result in
- out "Locate Query:
";
- MQueryUtil.text_of_query out query "";
- out "Result:
";
- MQueryUtil.text_of_result out result "
";
+ out (`Msg (`T "Locate Query:")) ;
+ MQueryUtil.text_of_query (fun m -> out (`Msg (`T m))) "" query;
+ out (`Msg (`T "Result:")) ;
+ MQueryUtil.text_of_result (fun m -> out (`Msg (`T m))) "" result;
user_uri_choice ~title:"Ambiguous input."
~msg:
("Ambiguous input \"" ^ id ^
@@ -1031,25 +966,25 @@ let input_or_locate_uri ~title =
ignore
(cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
let check_callback () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let uri = "cic:" ^ manual_input#text in
try
ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
- output_html outputhtml "OK
" ;
+ output_html outputhtml (`Msg (`T "OK")) ;
true
with
Getter.Unresolved ->
output_html outputhtml
- ("URI " ^ uri ^
- " does not correspond to any object.
") ;
+ (`Error (`T ("URI " ^ uri ^
+ " does not correspond to any object."))) ;
false
| UriManager.IllFormedUri _ ->
output_html outputhtml
- ("URI " ^ uri ^ " is not well-formed.
") ;
+ (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ;
false
| e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e))) ;
false
in
ignore
@@ -1096,25 +1031,15 @@ exception AmbiguousInput;;
(* A WIDGET TO ENTER CIC TERMS *)
-module ChosenTermEditor = TexTermEditor;;
-module ChosenTextualParser0 = TexCicTextualParser0;;
-(*
-module ChosenTermEditor = TermEditor;;
-module ChosenTextualParser0 = CicTextualParser0;;
-*)
-
module Callbacks =
struct
- let get_metasenv () = !ChosenTextualParser0.metasenv
- let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
-
- let output_html msg = output_html (outputhtml ()) msg;;
+ let output_html ?append_NL = output_html ?append_NL (outputhtml ())
let interactive_user_uri_choice =
fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
interactive_user_uri_choice ~selection_mode ?ok
- ?enable_button_for_non_vars ~title ~msg;;
- let interactive_interpretation_choice = interactive_interpretation_choice;;
- let input_or_locate_uri = input_or_locate_uri;;
+ ?enable_button_for_non_vars ~title ~msg
+ let interactive_interpretation_choice = interactive_interpretation_choice
+ let input_or_locate_uri = input_or_locate_uri
end
;;
@@ -1124,7 +1049,7 @@ module TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
let locate () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
match
GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
@@ -1136,7 +1061,7 @@ let locate () =
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
")
+ (`Error (`T (Printexc.to_string e)))
;;
@@ -1145,7 +1070,7 @@ exception NotAUriToAConstant;;
let new_inductive () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
@@ -1245,7 +1170,7 @@ let new_inductive () =
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
))
(* Second phase *)
and phase2 () =
@@ -1267,7 +1192,7 @@ let new_inductive () =
TexTermEditor'.term_editor
mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
(*non_empty_type := b ;*)
@@ -1352,7 +1277,7 @@ let new_inductive () =
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
))
(* Third phase *)
and phase3 name cons =
@@ -1379,7 +1304,7 @@ let new_inductive () =
TexTermEditor'.term_editor
mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
(* (*non_empty_type := b ;*)
@@ -1426,7 +1351,7 @@ let new_inductive () =
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
)) ;
window2#show () ;
GtkThread.main ();
@@ -1451,7 +1376,7 @@ let new_inductive () =
(*CSC: Da finire *)
let params = [] in
let tys = !get_types_and_cons () in
- let obj = Cic.InductiveDefinition tys params !paramsno in
+ let obj = Cic.InductiveDefinition(tys,params,!paramsno) in
begin
try
prerr_endline (CicPp.ppobj obj) ;
@@ -1472,12 +1397,12 @@ let new_inductive () =
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let new_proof () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
@@ -1526,19 +1451,14 @@ let new_proof () =
TexTermEditor'.term_editor
mqi_handle
~width:400 ~height:100 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
non_empty_type := b ;
okb#misc#set_sensitive (b && uri_entry#text <> ""))
in
let _ =
-let xxx = inputt#get_as_string in
-prerr_endline ("######################## " ^ xxx) ;
- newinputt#set_term xxx ;
-(*
- newinputt#set_term inputt#get_as_string ;
-*)
+ newinputt#set_term inputt#get_as_string ;
inputt#reset in
let _ =
uri_entry#connect#changed
@@ -1571,7 +1491,7 @@ prerr_endline ("######################## " ^ xxx) ;
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
)) ;
window#show () ;
GtkThread.main ();
@@ -1581,7 +1501,7 @@ prerr_endline ("######################## " ^ xxx) ;
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
ProofEngine.set_proof
(Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
- ProofEngine.goal := Some 1 ;
+ set_proof_engine_goal (Some 1) ;
refresh_goals notebook ;
refresh_proof output ;
!save_set_sensitive true ;
@@ -1592,15 +1512,15 @@ prerr_endline ("######################## " ^ xxx) ;
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let check_term_in_scratch scratch_window metasenv context expr =
@@ -1620,7 +1540,7 @@ let check_term_in_scratch scratch_window metasenv context expr =
let check scratch_window () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let metasenv =
match ProofEngine.get_proof () with
None -> []
@@ -1641,23 +1561,23 @@ let check scratch_window () =
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let show () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
show_in_show_window_uri (input_or_locate_uri ~title:"Show")
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
;;
exception NotADefinition;;
let open_ () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
try
@@ -1671,24 +1591,23 @@ let open_ () =
| Cic.Variable _
| Cic.InductiveDefinition _ -> raise NotADefinition
in
- ProofEngine.set_proof
- (Some (uri, metasenv, bo, ty)) ;
- ProofEngine.goal := None ;
+ ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ set_proof_engine_goal None ;
refresh_goals notebook ;
refresh_proof output ;
!save_set_sensitive true
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "
")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let show_query_results results =
@@ -1929,7 +1848,7 @@ let refine_constraints (must_obj,must_rel,must_sort) =
let completeSearchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
let must = CGSearchPattern.get_constraints expr in
@@ -1942,11 +1861,11 @@ let completeSearchPattern () =
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let insertQuery () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
let chosen = ref None in
let window =
@@ -1959,7 +1878,7 @@ let insertQuery () =
let scrolled_window =
GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
- let input = GEdit.text ~editable:true
+ let input = GText.view ~editable:true
~packing:scrolled_window#add () in
let hbox =
GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1977,7 +1896,7 @@ let insertQuery () =
ignore
(okb#connect#clicked
(function () ->
- chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
+ chosen := Some (input#buffer#get_text ()) ; window#destroy ())) ;
ignore
(loadb#connect#clicked
(function () ->
@@ -1995,8 +1914,8 @@ let insertQuery () =
End_of_file -> ""
in
let text = read_file () in
- input#delete_text 0 input#length ;
- ignore (input#insert_text text ~pos:0))) ;
+ input#buffer#delete input#buffer#start_iter input#buffer#end_iter ;
+ ignore (input#buffer#insert text))) ;
window#set_position `CENTER ;
window#show () ;
GtkThread.main ();
@@ -2010,7 +1929,7 @@ let insertQuery () =
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let choose_must list_of_must only =
@@ -2086,7 +2005,7 @@ let choose_must list_of_must only =
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
let clist =
GList.clist ~columns:2 ~packing:scrolled_window#add
- ~selection_mode:`EXTENDED
+ ~selection_mode:`MULTIPLE
~titles:["URI" ; "Position"] ()
in
ignore
@@ -2140,7 +2059,7 @@ let choose_must list_of_must only =
let searchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
let proof =
match ProofEngine.get_proof () with
@@ -2153,8 +2072,8 @@ let searchPattern () =
let uris' =
TacticChaser.matchConclusion
mqi_handle
- ~output_html:(output_html outputhtml) ~choose_must ()
- ~status:(proof, metano)
+ ~output_html:(fun m -> output_html outputhtml (`Msg (`T m)))
+ ~choose_must () ~status:(proof, metano)
in
let uri' =
user_uri_choice ~title:"Ambiguous input."
@@ -2166,7 +2085,7 @@ let searchPattern () =
with
e ->
output_html outputhtml
- ("" ^ Printexc.to_string e ^ "
")
+ (`Error (`T (Printexc.to_string e)))
;;
let choose_selection mmlwidget (element : Gdome.element option) =
@@ -2199,6 +2118,7 @@ let choose_selection mmlwidget (element : Gdome.element option) =
(* Stuff for the widget settings *)
+(*
let export_to_postscript output =
let lastdir = ref (Unix.getcwd ()) in
function () ->
@@ -2211,7 +2131,9 @@ let export_to_postscript output =
(output :> GMathView.math_view)#export_to_postscript
~filename:filename ();
;;
+*)
+(*
let activate_t1 output button_set_anti_aliasing
button_set_transparency export_to_postscript_menu_item
button_t1 ()
@@ -2240,6 +2162,7 @@ let set_anti_aliasing output button_set_anti_aliasing () =
let set_transparency output button_set_transparency () =
output#set_transparency button_set_transparency#active
;;
+*)
let changefont output font_size_spinb () =
output#set_font_size font_size_spinb#value_as_int
@@ -2302,14 +2225,18 @@ object(self)
button_set_anti_aliasing#misc#set_sensitive false ;
button_set_transparency#misc#set_sensitive false ;
(* Signals connection *)
+ (*
ignore(button_t1#connect#clicked
(activate_t1 output button_set_anti_aliasing
button_set_transparency export_to_postscript_menu_item button_t1)) ;
+ *)
ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
+ (*
ignore(button_set_anti_aliasing#connect#toggled
(set_anti_aliasing output button_set_anti_aliasing));
ignore(button_set_transparency#connect#toggled
(set_transparency output button_set_transparency)) ;
+ *)
ignore(log_verbosity_spinb#connect#changed
(set_log_verbosity output log_verbosity_spinb)) ;
ignore(closeb#connect#clicked settings_window#misc#hide)
@@ -2652,7 +2579,7 @@ object(self)
if not skip then
try
let (metano,setgoal,page) = List.nth !pages i in
- ProofEngine.goal := Some metano ;
+ set_proof_engine_goal (Some metano) ;
Lazy.force (page#compute) ;
Lazy.force setgoal;
if notify_hbugs_on_goal_change then
@@ -2665,32 +2592,30 @@ end
let dump_environment () =
try
let oc = open_out environmentfile in
- output_html (outputhtml ()) "Dumping environment ...
";
+ output_html (outputhtml ()) (`Msg (`T "Dumping environment ..."));
CicEnvironment.dump_to_channel
- ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
"))
+ ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri)))
oc;
- output_html (outputhtml ()) "... done!
";
+ output_html (outputhtml ()) (`Msg (`T "... done!")) ;
close_out oc
with exc ->
output_html (outputhtml ())
- (Printf.sprintf
- "Dump failure, uncaught exception:%s
"
- (Printexc.to_string exc))
+ (`Error (`T (Printf.sprintf "Dump failure, uncaught exception:%s"
+ (Printexc.to_string exc))))
;;
let restore_environment () =
try
let ic = open_in environmentfile in
- output_html (outputhtml ()) "Restoring environment ...
";
+ output_html (outputhtml ()) (`Msg (`T "Restoring environment ... "));
CicEnvironment.restore_from_channel
- ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
"))
+ ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri)))
ic;
- output_html (outputhtml ()) "... done!
";
+ output_html (outputhtml ()) (`Msg (`T "... done!"));
close_in ic
with exc ->
output_html (outputhtml ())
- (Printf.sprintf
- "Restore failure, uncaught exception:%s
"
- (Printexc.to_string exc))
+ (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s"
+ (Printexc.to_string exc))))
;;
(* Main window *)
@@ -2711,7 +2636,8 @@ class rendering_window output (notebook : notebook) =
(* file menu *)
let file_menu = factory0#add_submenu "File" in
let factory1 = new GMenu.factory file_menu ~accel_group in
- let export_to_postscript_menu_item =
+ (* let export_to_postscript_menu_item = *)
+ let _ =
begin
let _ =
factory1#add_item "New Block of (Co)Inductive Definitions..."
@@ -2746,13 +2672,15 @@ class rendering_window output (notebook : notebook) =
ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
ignore (!qed_set_sensitive false);
ignore (factory1#add_separator ()) ;
+ (*
let export_to_postscript_menu_item =
factory1#add_item "Export to PostScript..."
~callback:(export_to_postscript output) in
+ *)
ignore (factory1#add_separator ()) ;
ignore
- (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
- export_to_postscript_menu_item
+ (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) (*;
+ export_to_postscript_menu_item *)
end in
(* edit menu *)
let edit_menu = factory0#add_submenu "Edit Current Proof" in
@@ -2829,7 +2757,7 @@ class rendering_window output (notebook : notebook) =
factory3#add_item "Reload Stylesheets"
~callback:
(function _ ->
- ApplyStylesheets.reload_stylesheets () ;
+ ChosenTransformer.reload_stylesheets () ;
if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
@@ -2837,13 +2765,13 @@ class rendering_window output (notebook : notebook) =
with
InvokeTactics.RefreshSequentException e ->
output_html (outputhtml ())
- ("An error occurred while refreshing the " ^
- "sequent: " ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T ("An error occurred while refreshing the " ^
+ "sequent: " ^ Printexc.to_string e))) ;
(*notebook#remove_all_pages ~skip_switch_page_event:false ;*)
notebook#set_empty_page
| InvokeTactics.RefreshProofException e ->
output_html (outputhtml ())
- ("An error occurred while refreshing the proof: " ^ Printexc.to_string e ^ "
") ;
+ (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ;
output#unload
) in
(* accel group *)
@@ -2880,10 +2808,8 @@ class rendering_window output (notebook : notebook) =
GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
in
let outputhtml =
- GHtml.xmhtml
- ~source:""
+ new Ui_logger.html_logger
~width:400 ~height: 100
- ~border_width:20
~packing:frame#add
~show:true () in
object
@@ -2895,7 +2821,7 @@ object
method show = window#show
initializer
notebook#set_empty_page ;
- export_to_postscript_menu_item#misc#set_sensitive false ;
+ (*export_to_postscript_menu_item#misc#set_sensitive false ;*)
check_term := (check_term_in_scratch scratch_window) ;
(* signal handlers here *)
@@ -2906,13 +2832,12 @@ object
)) ;
ignore (output#connect#click (show_in_show_window_callback output)) ;
let settings_window = new settings_window output scrolled_window0
- export_to_postscript_menu_item (choose_selection output) in
+ (*export_to_postscript_menu_item*)() (choose_selection output) in
set_settings_window settings_window ;
set_outputhtml outputhtml ;
ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
- Logger.log_callback :=
- (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
-end;;
+ CicLogger.log_callback := (outputhtml#log_cic_msg ~append_NL:true)
+end
(* MAIN *)
@@ -2923,8 +2848,7 @@ let initialize_everything () =
let rendering_window' = new rendering_window output notebook in
set_rendering_window rendering_window' ;
let print_error_as_html prefix msg =
- output_html (outputhtml ())
- ("" ^ prefix ^ msg ^ "
")
+ output_html (outputhtml ()) (`Error (`T (prefix ^ msg)))
in
Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: "));
Gdome_xslt.setDebugCallback