From 0c69106b8cf67a0baad545a9d7b0816b2b7de8ac Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 21 Dec 2010 14:42:08 +0000 Subject: [PATCH] VERY EXPERIMENTAL: first version of Matita as a Tabbed Document Interface. The semantics of working on two tabs at the same time is not defined (yet? ...) --- matita/matita/.depend | 26 ++- matita/matita/.depend.opt | 26 ++- matita/matita/Makefile | 3 + matita/matita/cicMathView.ml | 4 +- matita/matita/matita.glade | 16 +- matita/matita/matita.ml | 73 +------ matita/matita/matitaGui.ml | 338 ++++++++++++++++--------------- matita/matita/matitaGuiTypes.mli | 1 + matita/matita/matitaMathView.ml | 14 +- matita/matita/matitaMathView.mli | 2 +- matita/matita/matitaScript.ml | 73 ++++--- matita/matita/matitaScript.mli | 9 +- 12 files changed, 278 insertions(+), 307 deletions(-) diff --git a/matita/matita/.depend b/matita/matita/.depend index 0d51469a6..b2221fe0b 100644 --- a/matita/matita/.depend +++ b/matita/matita/.depend @@ -22,10 +22,10 @@ matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \ matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi -matitaGui.cmo: virtuals.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ +matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaMathView.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmo \ matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi -matitaGui.cmx: virtuals.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ +matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \ matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi @@ -40,18 +40,16 @@ matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ matitaMathView.cmi matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi -matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ - matitaMathView.cmi matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi \ - buildTimeConf.cmo -matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ - matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ - buildTimeConf.cmx -matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMathView.cmi \ - matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi buildTimeConf.cmo \ - matitaScript.cmi -matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMathView.cmx \ - matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx buildTimeConf.cmx \ - matitaScript.cmi +matita.cmo: predefined_virtuals.cmi matitaScript.cmi matitaInit.cmi \ + matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo +matita.cmx: predefined_virtuals.cmx matitaScript.cmx matitaInit.cmx \ + matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx +matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \ + buildTimeConf.cmo matitaScript.cmi +matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \ + buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt index ccf85d10f..fb6531fb0 100644 --- a/matita/matita/.depend.opt +++ b/matita/matita/.depend.opt @@ -22,10 +22,10 @@ matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi -matitaGui.cmo: virtuals.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ +matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaMathView.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmx \ matitaExcPp.cmi buildTimeConf.cmx matitaGui.cmi -matitaGui.cmx: virtuals.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ +matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \ matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi @@ -40,18 +40,16 @@ matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ matitaMathView.cmi matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi -matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ - matitaMathView.cmi matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi \ - buildTimeConf.cmx -matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ - matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ - buildTimeConf.cmx -matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMathView.cmi \ - matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi buildTimeConf.cmx \ - matitaScript.cmi -matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMathView.cmx \ - matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx buildTimeConf.cmx \ - matitaScript.cmi +matita.cmo: predefined_virtuals.cmi matitaScript.cmi matitaInit.cmi \ + matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmx +matita.cmx: predefined_virtuals.cmx matitaScript.cmx matitaInit.cmx \ + matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx +matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \ + buildTimeConf.cmx matitaScript.cmi +matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \ + buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi diff --git a/matita/matita/Makefile b/matita/matita/Makefile index 0271b714a..0084e5e42 100644 --- a/matita/matita/Makefile +++ b/matita/matita/Makefile @@ -38,14 +38,17 @@ MLI = \ matitaTypes.mli \ matitaMisc.mli \ applyTransformation.mli \ + applyTransformationMml.mli \ matitaEngine.mli \ matitaExcPp.mli \ matitaInit.mli \ matitaGtkMisc.mli \ virtuals.mli \ cicMathView.mli \ + cicMathViewMml.mli \ predefined_virtuals.mli \ matitaMathView.mli \ + matitaMathViewMml.mli \ matitaScript.mli \ matitaGui.mli \ $(NULL) diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml index 2fe7db06b..02908dfd7 100644 --- a/matita/matita/cicMathView.ml +++ b/matita/matita/cicMathView.ml @@ -202,7 +202,7 @@ object (self) self#misc#modify_font_by_name (sprintf "%s %d" BuildTimeConf.script_font size)) -(* MATITA1.0 +(* MATITA 1.0 inherit GMathViewAux.multi_selection_math_view obj val mutable href_callback: (string -> unit) option = None @@ -616,7 +616,7 @@ object (self) self#thaw | _ -> *) - (* MATITA1.0 if BuildTimeConf.debug then begin + (* MATITA 1.0 if BuildTimeConf.debug then begin let name = "/tmp/cic_browser_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in HLog.debug ("cic_browser: dumping MathML to ./" ^ name); diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade index 6d4b59672..a49c5539d 100644 --- a/matita/matita/matita.glade +++ b/matita/matita/matita.glade @@ -1681,23 +1681,11 @@ True True - - True - True - automatic - automatic - - - - + - - True - script - + - False tab diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index 240a614f2..9ea693344 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -40,62 +40,13 @@ let _ = MatitaInit.initialize_all () ;; -(* let _ = Saturation.init () (* ALB to link paramodulation *) *) - -(** {2 GUI callbacks} *) - -let gui = MatitaGui.instance () - -let script = - 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 () ;; - (* math viewers *) -let _ = - let sequents_viewer = MatitaMathView.sequentsViewer_instance () in - sequents_viewer#load_logo; - let browser_observer _ = MatitaMathView.refresh_all_browsers () in - let sequents_observer grafite_status = - sequents_viewer#reset; - match grafite_status#ng_mode with - `ProofMode -> - sequents_viewer#nload_sequents grafite_status; - (try - script#setGoal - (Some (Continuationals.Stack.find_goal grafite_status#stack)); - let goal = - match script#goal with - None -> assert false - | Some n -> n - in - sequents_viewer#goto_sequent grafite_status goal - with Failure _ -> script#setGoal None); - | `CommandMode -> sequents_viewer#load_logo - in - script#addObserver sequents_observer; - script#addObserver browser_observer -;; - (** {{{ Debugging *) -let _ = +let init_debugging_menu gui = if BuildTimeConf.debug || Helm_registry.get_bool "matita.debug_menu" then begin @@ -116,7 +67,7 @@ let _ = ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ()) in addDebugItem "dump aliases" (fun _ -> - let status = script#grafite_status in + let status = (MatitaScript.current ())#grafite_status in GrafiteDisambiguate.dump_aliases prerr_endline "" status); (* FG: DEBUGGING addDebugItem "dump interpretations" (fun _ -> @@ -159,20 +110,16 @@ let _ = at_exit (fun () -> print_endline "\nThanks for using Matita!\n"); Sys.catch_break true; let args = Helm_registry.get_list Helm_registry.string "matita.args" in - (try gui#loadScript (List.hd args) with Failure _ -> ()); + let gui = MatitaGui.instance () in + init_debugging_menu gui; + if args = [] then + gui#newScript () + else + List.iter gui#loadScript (List.rev args); gui#main#mainWin#show (); try GtkThread.main () - with Sys.Break -> - Sys.set_signal Sys.sigint - (Sys.Signal_handle - (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 - LibraryClean.clean_baseuris [baseuri] + with Sys.Break -> () +;; (* vim:set foldmethod=marker: *) diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 5217abeb2..91276e0dd 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -37,6 +37,76 @@ let all_disambiguation_passes = ref false let gui_instance = ref None +(* this is a shit and should be changed :-{ *) +let interactive_uri_choice + ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "") + ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) + ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO) + ?copy_cb () + ~id uris += + let gui = MatitaMisc.get_gui () in + if (selection_mode <> `SINGLE) && + (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation") + then + uris + else begin + let dialog = gui#newUriDialog () in + if hide_uri_entry then + dialog#uriEntryHBox#misc#hide (); + if hide_try then + begin + dialog#uriChoiceSelectedButton#misc#hide (); + dialog#uriChoiceConstantsButton#misc#hide (); + end; + dialog#okLabel#set_label ok_label; + dialog#uriChoiceTreeView#selection#set_mode + (selection_mode :> Gtk.Tags.selection_mode); + let model = new stringListModel dialog#uriChoiceTreeView in + let choices = ref None in + (match copy_cb with + | None -> () + | Some cb -> + dialog#copyButton#misc#show (); + connect_button dialog#copyButton + (fun _ -> + match model#easy_selection () with + | [u] -> (cb u) + | _ -> ())); + dialog#uriChoiceDialog#set_title title; + dialog#uriChoiceLabel#set_text msg; + List.iter model#easy_append (List.map NReference.string_of_reference uris); + dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; + let return v = + choices := v; + dialog#uriChoiceDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#uriChoiceConstantsButton (fun _ -> + return (Some uris)); + if ok_action = `AUTO then + connect_button dialog#uriChoiceAutoButton (fun _ -> + Helm_registry.set_bool "matita.auto_disambiguation" true; + return (Some uris)) + else + connect_button dialog#uriChoiceAutoButton (fun _ -> + match model#easy_selection () with + | [] -> () + | uris -> return (Some (List.map NReference.reference_of_string uris))); + connect_button dialog#uriChoiceSelectedButton (fun _ -> + match model#easy_selection () with + | [] -> () + | uris -> return (Some (List.map NReference.reference_of_string uris))); + connect_button dialog#uriChoiceAbortButton (fun _ -> return None); + dialog#uriChoiceDialog#show (); + GtkThread.main (); + (match !choices with + | None -> raise MatitaTypes.Cancel + | Some uris -> uris) + end + + class type browserWin = (* this class exists only because GEdit.combo_box_entry is not supported by * lablgladecc :-(((( *) @@ -80,10 +150,10 @@ let save_moo grafite_status = | _ -> clean_current_baseuri grafite_status ;; -let ask_unsaved parent = +let ask_unsaved parent filename = MatitaGtkMisc.ask_confirmation ~parent ~title:"Unsaved work!" - ~message:("Your work is unsaved!\n\n"^ + ~message:("Script " ^ filename ^ " is modified.!\n\n"^ "Do you want to save the script before continuing?") () @@ -345,13 +415,14 @@ let interactive_error_interp ~all_passes class gui () = (* creation order _is_ relevant for windows placement *) let main = new mainWin () in + let sequents_viewer = + MatitaMathView.sequentsViewer_instance main#sequentsNotebook in let fileSel = new fileSelectionWin () in let findRepl = new findReplWin () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ main#mainWinEventBox ] in let console = new console ~buffer:main#logTextView#buffer () in - let source_view () = (MatitaScript.current ())#source_view in object (self) val mutable chosen_file = None val mutable _ok_not_exists = false @@ -420,7 +491,7 @@ class gui () = in let hide_find_Repl () = findRepl#toplevel#misc#hide () in let find_forward _ = - let source_view = source_view () in + let source_view = (s ())#source_view in let highlight start end_ = source_view#source_buffer#move_mark `INSERT ~where:start; source_view#source_buffer#move_mark `SEL_BOUND ~where:end_; @@ -436,7 +507,7 @@ class gui () = | Some (start,end_) -> highlight start end_ in let replace _ = - let source_view = source_view () in + let source_view = (s ())#source_view in let text = findRepl#replaceEntry#text in let ins = source_view#source_buffer#get_iter `INSERT in let sel = source_view#source_buffer#get_iter `SEL_BOUND in @@ -485,7 +556,7 @@ class gui () = connect_menu_item main#pastePatternMenuItem (fun () -> (MatitaScript.current ())#pastePattern ()); connect_menu_item main#selectAllMenuItem (fun () -> - let source_view = source_view () in + let source_view = (s ())#source_view in source_view#source_buffer#move_mark `INSERT source_view#source_buffer#start_iter; source_view#source_buffer#move_mark `SEL_BOUND source_view#source_buffer#end_iter); connect_menu_item main#findReplMenuItem show_find_Repl; @@ -495,13 +566,13 @@ class gui () = ignore (findRepl#findEntry#connect#activate find_forward); (* interface lockers *) let lock_world _ = - let source_view = source_view () in + let source_view = (s ())#source_view in main#buttonsToolbar#misc#set_sensitive false; main#scriptMenu#misc#set_sensitive false; source_view#set_editable false in let unlock_world _ = - let source_view = source_view () in + let source_view = (s ())#source_view in main#buttonsToolbar#misc#set_sensitive true; main#scriptMenu#misc#set_sensitive true; source_view#set_editable true; @@ -643,48 +714,48 @@ class gui () = else main#tacticsButtonsHandlebox#misc#hide ()) ~check:main#menuitemPalette; connect_button main#butImpl_intro - (fun () -> (source_view ())#source_buffer#insert "apply rule (⇒#i […] (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (⇒#i […] (…));\n"); connect_button main#butAnd_intro - (fun () -> (source_view ())#source_buffer#insert + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∧#i (…) (…));\n\t[\n\t|\n\t]\n"); connect_button main#butOr_intro_left - (fun () -> (source_view ())#source_buffer#insert "apply rule (∨#i_l (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∨#i_l (…));\n"); connect_button main#butOr_intro_right - (fun () -> (source_view ())#source_buffer#insert "apply rule (∨#i_r (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∨#i_r (…));\n"); connect_button main#butNot_intro - (fun () -> (source_view ())#source_buffer#insert "apply rule (¬#i […] (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (¬#i […] (…));\n"); connect_button main#butTop_intro - (fun () -> (source_view ())#source_buffer#insert "apply rule (⊤#i);\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (⊤#i);\n"); connect_button main#butImpl_elim - (fun () -> (source_view ())#source_buffer#insert + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (⇒#e (…) (…));\n\t[\n\t|\n\t]\n"); connect_button main#butAnd_elim_left - (fun () -> (source_view ())#source_buffer#insert "apply rule (∧#e_l (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∧#e_l (…));\n"); connect_button main#butAnd_elim_right - (fun () -> (source_view ())#source_buffer#insert "apply rule (∧#e_r (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∧#e_r (…));\n"); connect_button main#butOr_elim - (fun () -> (source_view ())#source_buffer#insert + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∨#e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n"); connect_button main#butNot_elim - (fun () -> (source_view ())#source_buffer#insert + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (¬#e (…) (…));\n\t[\n\t|\n\t]\n"); connect_button main#butBot_elim - (fun () -> (source_view ())#source_buffer#insert "apply rule (⊥#e (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (⊥#e (…));\n"); connect_button main#butRAA - (fun () -> (source_view ())#source_buffer#insert "apply rule (RAA […] (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (RAA […] (…));\n"); connect_button main#butUseLemma - (fun () -> (source_view ())#source_buffer#insert "apply rule (lem #premises name …);\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (lem #premises name …);\n"); connect_button main#butDischarge - (fun () -> (source_view ())#source_buffer#insert "apply rule (discharge […]);\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (discharge […]);\n"); connect_button main#butForall_intro - (fun () -> (source_view ())#source_buffer#insert "apply rule (∀#i {…} (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∀#i {…} (…));\n"); connect_button main#butForall_elim - (fun () -> (source_view ())#source_buffer#insert "apply rule (∀#e {…} (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∀#e {…} (…));\n"); connect_button main#butExists_intro - (fun () -> (source_view ())#source_buffer#insert "apply rule (∃#i {…} (…));\n"); + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∃#i {…} (…));\n"); connect_button main#butExists_elim - (fun () -> (source_view ())#source_buffer#insert + (fun () -> (s ())#source_view#source_buffer#insert "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n"); @@ -700,7 +771,7 @@ class gui () = let status = Interpretations.toggle_active_interpretations s#grafite_status b in - assert false (* MATITA1.0 ??? + assert false (* MATITA 1.0 ??? s#set_grafite_status status*) ); MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem @@ -717,15 +788,15 @@ class gui () = | MatitaScript.ActionCancelled s -> HLog.error s | exn -> if not (Helm_registry.get_bool "matita.debug") then - (*CSC: MatitaScript.current ??? *) + (* MatitaScript.current is problably wrong, but what else + can we do? *) notify_exn (MatitaScript.current ())#source_view exn else raise exn); let disableSave () = (s())#assignFileName None; main#saveMenuItem#misc#set_sensitive false in - let saveAsScript () = - let script = s () in + let saveAsScript script = match self#chooseFile ~ok_not_exists:true () with | Some f -> HExtlib.touch f; @@ -735,53 +806,21 @@ class gui () = self#_enableSaveTo f | None -> () in - let saveScript () = - let script = s () in + let saveScript script = if script#has_name then (script#saveToFile (); - console#message ("'"^script#filename^"' saved.\n")) - else saveAsScript () - in - let abandon_script () = - let source_view = source_view () in - let grafite_status = (s ())#grafite_status in - if source_view#buffer#modified then - (match ask_unsaved main#toplevel with - | `YES -> saveScript () - | `NO -> () - | `CANCEL -> raise MatitaTypes.Cancel); - save_moo grafite_status + console#message ("'"^script#filename^"' saved.\n")) + else saveAsScript script in let loadScript () = - let source_view = source_view () in - let script = s () in try match self#chooseFile () with - | Some f -> - abandon_script (); - script#reset (); - script#assignFileName (Some f); - source_view#source_buffer#begin_not_undoable_action (); - script#loadFromFile f; - source_view#source_buffer#end_not_undoable_action (); - source_view#buffer#move_mark `INSERT source_view#buffer#start_iter; - source_view#buffer#place_cursor source_view#buffer#start_iter; - console#message ("'"^f^"' loaded.\n"); - self#_enableSaveTo f + | Some f -> self#loadScript f | None -> () with MatitaTypes.Cancel -> () in - let newScript () = - let source_view = source_view () in - abandon_script (); - source_view#source_buffer#begin_not_undoable_action (); - (s ())#reset (); - (s ())#template (); - source_view#source_buffer#end_not_undoable_action (); - disableSave () - in let cursor () = - let source_view = source_view () in + let source_view = (s ())#source_view in source_view#source_buffer#place_cursor (source_view#source_buffer#get_iter_at_mark (`NAME "locked")) in let advance (script: MatitaScript.script) = script#advance (); cursor () in @@ -796,19 +835,23 @@ class gui () = let jump () = locker (keep_focus jump) (MatitaScript.current ()) in (* quit *) self#setQuitCallback (fun () -> -(*CSC: iterare su tutti gli script! - let script = MatitaScript.current () in - if source_view#buffer#modified then - match ask_unsaved main#toplevel with - | `YES -> - saveScript (); - save_moo script#grafite_status; - GMain.Main.quit () - | `NO -> GMain.Main.quit () - | `CANCEL -> () - else - (save_moo script#grafite_status; - GMain.Main.quit ())*) assert false); + let cancel = ref false in + MatitaScript.iter_scripts + (fun script -> + if not !cancel then + if script#source_view#buffer#modified then + match + ask_unsaved main#toplevel (Filename.basename script#filename) + with + | `YES -> + saveScript script; + save_moo script#grafite_status + | `NO -> () + | `CANCEL -> cancel := true + else + save_moo script#grafite_status); + if not !cancel then + GMain.Main.quit ()); connect_button main#scriptAdvanceButton advance; connect_button main#scriptRetractButton retract; connect_button main#scriptTopButton top; @@ -821,9 +864,11 @@ class gui () = connect_menu_item main#scriptBottomMenuItem bottom; connect_menu_item main#scriptJumpMenuItem jump; connect_menu_item main#openMenuItem loadScript; - connect_menu_item main#saveMenuItem saveScript; - connect_menu_item main#saveAsMenuItem saveAsScript; - connect_menu_item main#newMenuItem newScript; + connect_menu_item main#saveMenuItem + (fun () -> saveScript (MatitaScript.current ())); + connect_menu_item main#saveAsMenuItem + (fun () -> saveAsScript (MatitaScript.current ())); + connect_menu_item main#newMenuItem self#newScript; connect_menu_item main#showCoercionsGraphMenuItem (fun _ -> let c = MatitaMathView.cicBrowser () in @@ -871,7 +916,8 @@ class gui () = MatitaMisc.reset_font_size; method private externalEditor () = - let source_view = source_view () in + let script = MatitaScript.current () in + let source_view = script#source_view in let cmd = Helm_registry.get "matita.external_editor" in (* ZACK uncomment to enable interactive ask of external editor command *) (* let cmd = @@ -884,7 +930,6 @@ class gui () = ask_text ~gui:self ~title:"External editor" ~msg ~multiline:false ~default:(Helm_registry.get "matita.external_editor") () in *) - let script = MatitaScript.current () in let fname = script#filename in let slice mark = source_view#source_buffer#start_iter#get_slice @@ -927,9 +972,55 @@ class gui () = | Exit -> () | Invalid_argument _ -> script#goto `Bottom () + method newScript () = + let scrolledWindow = GBin.scrolled_window () in + let tab_label = GMisc.label ~text:"foo" () in + ignore (main#scriptNotebook#prepend_page ~tab_label:tab_label#coerce scrolledWindow#coerce); + let script = + MatitaScript.script + ~urichooser:(fun source_view uris -> + try + 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:(MatitaMisc.get_gui ())#main#toplevel ()) + ~parent:scrolledWindow ~tab_label () + in + main#scriptNotebook#goto_page 0; + sequents_viewer#reset; + sequents_viewer#load_logo; + let browser_observer _ = MatitaMathView.refresh_all_browsers () in + let sequents_observer grafite_status = + sequents_viewer#reset; + match grafite_status#ng_mode with + `ProofMode -> + sequents_viewer#nload_sequents grafite_status; + (try + script#setGoal + (Some (Continuationals.Stack.find_goal grafite_status#stack)); + let goal = + match script#goal with + None -> assert false + | Some n -> n + in + sequents_viewer#goto_sequent grafite_status goal + with Failure _ -> script#setGoal None); + | `CommandMode -> sequents_viewer#load_logo + in + script#addObserver sequents_observer; + script#addObserver browser_observer + method loadScript file = - let source_view = source_view () in - let script = MatitaScript.current () in + self#newScript (); + let script = MatitaScript.current () in + let source_view = script#source_view in script#reset (); script#assignFileName (Some file); let file = script#filename in @@ -944,7 +1035,7 @@ class gui () = source_view#buffer#place_cursor source_view#buffer#start_iter; console#message ("'"^file^"' loaded."); self#_enableSaveTo file - + method private _enableSaveTo file = self#main#saveMenuItem#misc#set_sensitive true @@ -1036,75 +1127,6 @@ let instance = singleton gui let non p x = not (p x) -(* this is a shit and should be changed :-{ *) -let interactive_uri_choice - ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "") - ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) - ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO) - ?copy_cb () - ~id uris -= - let gui = instance () in - if (selection_mode <> `SINGLE) && - (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation") - then - uris - else begin - let dialog = gui#newUriDialog () in - if hide_uri_entry then - dialog#uriEntryHBox#misc#hide (); - if hide_try then - begin - dialog#uriChoiceSelectedButton#misc#hide (); - dialog#uriChoiceConstantsButton#misc#hide (); - end; - dialog#okLabel#set_label ok_label; - dialog#uriChoiceTreeView#selection#set_mode - (selection_mode :> Gtk.Tags.selection_mode); - let model = new stringListModel dialog#uriChoiceTreeView in - let choices = ref None in - (match copy_cb with - | None -> () - | Some cb -> - dialog#copyButton#misc#show (); - connect_button dialog#copyButton - (fun _ -> - match model#easy_selection () with - | [u] -> (cb u) - | _ -> ())); - dialog#uriChoiceDialog#set_title title; - dialog#uriChoiceLabel#set_text msg; - List.iter model#easy_append (List.map NReference.string_of_reference uris); - dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; - let return v = - choices := v; - dialog#uriChoiceDialog#destroy (); - GMain.Main.quit () - in - ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#uriChoiceConstantsButton (fun _ -> - return (Some uris)); - if ok_action = `AUTO then - connect_button dialog#uriChoiceAutoButton (fun _ -> - Helm_registry.set_bool "matita.auto_disambiguation" true; - return (Some uris)) - else - connect_button dialog#uriChoiceAutoButton (fun _ -> - match model#easy_selection () with - | [] -> () - | uris -> return (Some (List.map NReference.reference_of_string uris))); - connect_button dialog#uriChoiceSelectedButton (fun _ -> - match model#easy_selection () with - | [] -> () - | uris -> return (Some (List.map NReference.reference_of_string uris))); - connect_button dialog#uriChoiceAbortButton (fun _ -> return None); - dialog#uriChoiceDialog#show (); - GtkThread.main (); - (match !choices with - | None -> raise MatitaTypes.Cancel - | Some uris -> uris) - end - class interpModel = let cols = new GTree.column_list in let id_col = cols#add Gobject.Data.string in diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index 8e3932b04..fa62970ce 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -71,6 +71,7 @@ object (** prompt the user for a (multiline) text entry *) method askText: ?title:string -> ?msg:string -> unit -> string option + method newScript: unit -> unit method loadScript: string -> unit end diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index e00e4fdc5..e42f63ae2 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -680,12 +680,16 @@ let default_cicMathView () = let cicMathView_instance = MatitaMisc.singleton default_cicMathView -let default_sequentsViewer () = - let gui = MatitaMisc.get_gui () in +let default_sequentsViewer notebook = let cicMathView = cicMathView_instance () in - sequentsViewer ~notebook:gui#main#sequentsNotebook ~cicMathView () -let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer - + sequentsViewer ~notebook ~cicMathView () +let sequentsViewer_instance = + let already_used = ref false in + fun notebook -> + if !already_used then assert false + else + (already_used := true; + default_sequentsViewer notebook) (** @param reuse if set reused last opened cic browser otherwise * opens a new one. default is false *) diff --git a/matita/matita/matitaMathView.mli b/matita/matita/matitaMathView.mli index 51bba6b3e..32f095a0a 100644 --- a/matita/matita/matitaMathView.mli +++ b/matita/matita/matitaMathView.mli @@ -27,7 +27,7 @@ val cicBrowser: unit -> MatitaGuiTypes.cicBrowser (** {2 Singleton instances} *) -val sequentsViewer_instance: unit -> MatitaGuiTypes.sequentsViewer +val sequentsViewer_instance: GPack.notebook -> MatitaGuiTypes.sequentsViewer (** {2 Global changes} *) diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index a9a86bb80..f3f38ccac 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -254,14 +254,14 @@ let fresh_script_id = * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may * be added *) -class script ~ask_confirmation ~urichooser () = +class script ~ask_confirmation ~urichooser ~(parent:GBin.scrolled_window) ~tab_label () = let source_view = GSourceView2.source_view ~auto_indent:true ~insert_spaces_instead_of_tabs:true ~tab_width:2 ~right_margin_position:80 ~show_right_margin:true ~smart_home_end:`AFTER - ~packing:(MatitaMisc.get_gui ())#main#scriptScrolledWin#add + ~packing:parent#add_with_viewport () in let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in @@ -283,14 +283,17 @@ in let read_include_paths file = try let root, _buri, _fname, _tgt = - Librarian.baseuri_of_script ~include_paths:[] file - in - let rc = - Str.split (Str.regexp " ") - (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) + Librarian.baseuri_of_script ~include_paths:[] file in + let includes = + try + Str.split (Str.regexp " ") + (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) + with Not_found -> [] in - List.iter (HLog.debug) rc; rc - with Librarian.NoRootFor _ | Not_found -> [] + let rc = root :: includes in + List.iter (HLog.debug) rc; rc + with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> + [] in let default_buri = "cic:/matita/tests" in let default_fname = ".unnamed.ma" in @@ -323,7 +326,7 @@ object (self) method private curdir = try let root, _buri, _fname, _tgt = - Librarian.baseuri_of_script ~include_paths:self#include_paths + Librarian.baseuri_of_script ~include_paths:self#include_paths self#filename in root @@ -338,11 +341,16 @@ object (self) Librarian.baseuri_of_script ~include_paths:self#include_paths f in buri - with Librarian.NoRootFor _ -> default_buri + with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> default_buri method filename = match filename_ with None -> default_fname | Some f -> f initializer + ignore + (source_view#source_buffer#begin_not_undoable_action (); + self#reset (); + self#template (); + source_view#source_buffer#end_not_undoable_action ()); MatitaMisc.observe_font_size (fun font_size -> source_view#misc#modify_font_by_name (sprintf "%s %d" BuildTimeConf.script_font font_size)); @@ -438,11 +446,6 @@ object (self) menu#remove (redoMenuItem :> GMenu.menu_item); MatitaGtkMisc.connect_menu_item new_redoMenuItem (fun () -> self#safe_redo))); - ignore - (source_view#source_buffer#begin_not_undoable_action (); - self#reset (); - self#template (); - source_view#source_buffer#end_not_undoable_action ()) val mutable statements = [] (** executed statements *) @@ -842,24 +845,21 @@ object (self) method assignFileName file = match file with None -> - (MatitaMisc.get_gui ())#main#scriptLabel#set_text default_fname; + tab_label#set_text default_fname; filename_ <- None; include_paths_ <- []; self#reset_buffer | Some file -> let f = Librarian.absolutize file in - (MatitaMisc.get_gui ())#main#scriptLabel#set_text (Filename.basename f); + tab_label#set_text (Filename.basename f); filename_ <- Some f; include_paths_ <- read_include_paths f; - self#reset_buffer; - Sys.chdir self#curdir; - HLog.debug ("Moving to " ^ Sys.getcwd ()) + self#reset_buffer method set_star b = - let label = (MatitaMisc.get_gui ())#main#scriptLabel in - label#set_text ((if b then "*" else "") ^ Filename.basename self#filename); - label#misc#set_tooltip_text - ("URI: " ^ self#buri_of_current_file ^ "\nPATH: " ^ self#filename) + tab_label#set_text ((if b then "*" else "")^Filename.basename self#filename); + tab_label#misc#set_tooltip_text + ("URI: " ^ self#buri_of_current_file ^ "\nPATH: " ^ self#filename); method saveToFile () = if self#has_name then @@ -902,7 +902,7 @@ object (self) let template = HExtlib.input_file BuildTimeConf.script_template in buffer#insert ~iter:(buffer#get_iter `START) template; buffer#set_modified false; - self#set_star false + self#set_star false; method goto (pos: [`Top | `Bottom | `Cursor]) () = try @@ -1028,17 +1028,28 @@ object (self) HLog.debug (sprintf "%d statements:" (List.length statements)); List.iter HLog.debug statements; HLog.debug ("Current file name: " ^ self#filename); + + method has_parent (p : GObj.widget) = parent#coerce#misc#get_oid = p#misc#get_oid end -let _script = ref None +let _script = ref [] -let script ~urichooser ~ask_confirmation () +let script ~urichooser ~ask_confirmation ~parent ~tab_label () = - let s = new script ~ask_confirmation ~urichooser () in - _script := Some s; + let s = new script ~ask_confirmation ~urichooser ~parent ~tab_label () in + _script := s::!_script; s -let current () = match !_script with None -> assert false | Some s -> s +let current () = + let notebook = (MatitaMisc.get_gui ())#main#scriptNotebook in + let parent = notebook#get_nth_page notebook#current_page in + try + List.find (fun s -> s#has_parent parent) !_script + with + Not_found -> assert false +;; + +let iter_scripts f = List.iter f !_script;; let _ = CicMathView.register_matita_script_current (current :> unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit >) diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli index aab7488a4..5e8658d3f 100644 --- a/matita/matita/matitaScript.mli +++ b/matita/matita/matitaScript.mli @@ -99,6 +99,7 @@ object method clean_dirty_lock: unit method set_star: bool -> unit method source_view: GSourceView2.source_view + method has_parent: GObj.widget -> bool (* debug *) method dump : unit -> unit @@ -110,12 +111,10 @@ val script: urichooser: (GSourceView2.source_view -> NReference.reference list -> NReference.reference list) -> ask_confirmation: (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> + parent:GBin.scrolled_window -> + tab_label:GMisc.label -> unit -> script -(* each time script above is called an internal ref is set, instance will return - * the value of this ref *) -(* TODO Zack: orrible solution until we found a better one for having a single - * access point for the script *) val current: unit -> script - +val iter_scripts: (script -> unit) -> unit -- 2.39.2