let gui = MatitaGui.instance ()
let script =
- let s =
- MatitaScript.script
- ~source_view:gui#sourceView
- ~mathviewer:(MatitaMathView.mathViewer ())
- ~urichooser:(fun uris ->
- try
- MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
- ~title:"Matita: URI chooser"
- ~msg:"Select the URI" ~hide_uri_entry:true
- ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
- ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
- () ~id:"boh?" uris
- with MatitaTypes.Cancel -> [])
- ~set_star:gui#setStar
- ~ask_confirmation:
- (fun ~title ~message ->
- MatitaGtkMisc.ask_confirmation ~title ~message
- ~parent:gui#main#toplevel ())
- ()
- in
+ MatitaScript.script
+ ~urichooser:(fun source_view uris ->
+ try
+ MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
+ ~title:"Matita: URI chooser"
+ ~msg:"Select the URI" ~hide_uri_entry:true
+ ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
+ ~copy_cb:(fun s -> source_view#buffer#insert ("\n"^s^"\n"))
+ () ~id:"boh?" uris
+ with MatitaTypes.Cancel -> [])
+ ~ask_confirmation:
+ (fun ~title ~message ->
+ MatitaGtkMisc.ask_confirmation ~title ~message
+ ~parent:gui#main#toplevel ())
+ ()
+
+let _ =
Predefined_virtuals.load_predefined_virtuals ();
Predefined_virtuals.load_predefined_classes ();
- gui#sourceView#source_buffer#begin_not_undoable_action ();
- s#reset ();
- s#template ();
- gui#sourceView#source_buffer#end_not_undoable_action ();
- s
(* math viewers *)
let _ =
- let cic_math_view = MatitaMathView.cicMathView_instance () in
let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
sequents_viewer#load_logo;
- cic_math_view#set_href_callback
- (Some (fun uri ->
- let uri =
- try
- `Uri (UriManager.uri_of_string uri)
- with
- UriManager.IllFormedUri _ ->
- `NRef (NReference.reference_of_string uri)
- in
- (MatitaMathView.cicBrowser ())#load uri));
let browser_observer _ = MatitaMathView.refresh_all_browsers () in
let sequents_observer grafite_status =
sequents_viewer#reset;
in
addDebugItem "dump aliases" (fun _ ->
let status = script#grafite_status in
- LexiconEngine.dump_aliases prerr_endline "" status);
+ GrafiteDisambiguate.dump_aliases prerr_endline "" status);
(* FG: DEBUGGING
addDebugItem "dump interpretations" (fun _ ->
let status = script#lexicon_status in
*)
addDebugSeparator ();
addDebugCheckbox "high level pretty printer" ~init:true
- (fun mi () -> CicMetaSubst.use_low_level_ppterm_in_context := mi#active);
+ (fun mi () -> assert false (* MATITA 1.0 *));
addDebugSeparator ();
addDebugItem "always show all disambiguation errors"
(fun _ -> MatitaGui.all_disambiguation_passes := true);
(fun mi () -> NCicRefiner.debug := mi#active; NCicUnification.debug :=
mi#active; MultiPassDisambiguator.debug := mi#active; NCicMetaSubst.debug := mi#active);
addDebugCheckbox "reduction logging"
- (fun mi () -> NCicReduction.debug := mi#active; CicReduction.ndebug := mi#active);
+ (fun mi () -> NCicReduction.debug := mi#active);
addDebugSeparator ();
addDebugItem "Expand virtuals"
(fun _ -> (MatitaScript.current ())#expandAllVirtuals);
(fun _ ->
prerr_endline "Still cleaning the library: don't be impatient!"));
prerr_endline "Matita is cleaning up. Please wait.";
+ (*CSC: MatitaScript.current () makes no sense here *)
let baseuri =
(MatitaScript.current ())#grafite_status#baseuri
in