From: Stefano Zacchiroli Date: Tue, 9 Nov 2004 17:23:18 +0000 (+0000) Subject: snapshot, notably: X-Git-Tag: v_0_6_4_1~6 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=190e42f1030ea3d459c4040bb0e8503a7c096820;p=helm.git snapshot, notably: - fixed "noshow" bugs in sequents notebook and proof window - implemented interpretation choice --- diff --git a/helm/matita/.depend b/helm/matita/.depend index 4aadffba2..65c9fb8f3 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -16,8 +16,10 @@ matitaInterpreter.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGui.cmi \ matitaMathView.cmi matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi matitaInterpreter.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGui.cmx \ matitaMathView.cmx matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi -matitaMathView.cmo: matitaCicMisc.cmo matitaTypes.cmo matitaMathView.cmi -matitaMathView.cmx: matitaCicMisc.cmx matitaTypes.cmx matitaMathView.cmi +matitaMathView.cmo: matitaCicMisc.cmo matitaGui.cmi matitaTypes.cmo \ + matitaMathView.cmi +matitaMathView.cmx: matitaCicMisc.cmx matitaGui.cmx matitaTypes.cmx \ + matitaMathView.cmi matitaMisc.cmo: matitaMisc.cmi matitaMisc.cmx: matitaMisc.cmi matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \ diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index d04ac1867..d31611ba0 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -40,7 +40,6 @@ helm-tactics \ helm-xml \ helm-xmldiff \ helm-cic_textual_parser2 \ -helm-mathql_interpreter \ " for r in $FINDLIB_REQUIRES do diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index 1ca17a9ed..db02076cb 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -1,18 +1,20 @@ +
+ mowgli.cs.unibo.it + +
matita.glade true
- mowgli.cs.unibo.it - + $(prefs.server) helm mowgli
remote - http://mowgli.cs.unibo.it:58081/ - + http://$(prefs.server):58081/
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 4ecd6d46a..5aac61297 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -1475,6 +1475,7 @@ Copyright (C) 2004, + 200 Interpretation choice GTK_WINDOW_TOPLEVEL GTK_WIN_POS_NONE @@ -1553,7 +1554,7 @@ Copyright (C) 2004, 0 - + True some informative message here ... False @@ -1574,7 +1575,30 @@ Copyright (C) 2004, - + + True + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + + + + + 0 + True + True + @@ -1736,164 +1760,244 @@ Copyright (C) 2004, False - + True - False - 0 + True + True + True + GTK_POS_BOTTOM + False + False - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + False + 0 - + True - True - True - False + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - + True - go back 1 phrase - True - GTK_RELIEF_NORMAL - True + True + True + False - + True - gtk-go-back - 4 - 0.5 - 0.5 - 0 - 0 + go back 1 phrase + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-go-back + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + - - - False - False - - - - - True - True - True - False + + + True + True + True + False + + + + True + execute til cursor + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + - + True - execute til cursor - True - GTK_RELIEF_NORMAL - True + True + True + False - + True - gtk-jump-to - 4 - 0.5 - 0.5 - 0 - 0 + go forward 1 phrase + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-go-forward + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + + 0 False - False + False - + True - True - True - False + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT - + True - go forward 1 phrase True - GTK_RELIEF_NORMAL - True - - - - True - gtk-go-forward - 4 - 0.5 - 0.5 - 0 - 0 - - + True + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_NONE + True + 0 + 0 + 0 + 0 + 0 + 0 + - False - False + 0 + True + True - 0 - False - False + False + True + + + + + + True + script + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab - + True True GTK_POLICY_ALWAYS GTK_POLICY_ALWAYS - GTK_SHADOW_NONE + GTK_SHADOW_IN GTK_CORNER_TOP_LEFT - + True True - True - False - True - GTK_JUSTIFY_LEFT - GTK_WRAP_NONE - True - 0 - 0 - 0 - 0 - 0 - 0 - + False + False + False + True - 0 - True - True + False + True + + + + + + True + outline + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index e565c03a7..6a5e2e51d 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -61,13 +61,10 @@ let disambiguator = ~chooseUris:(interactive_user_uri_choice ~gui) ~chooseInterp:(interactive_interp_choice ~gui) () -let proof_viewer = - let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in - MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) () +let proof_viewer = MatitaMathView.proof_viewer_instance () let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () let sequents_viewer = let set_goal goal = - debug_print (sprintf "Setting goal %d" goal); if not (has_proof ()) then assert false; (get_proof ())#set_goal goal in @@ -77,12 +74,8 @@ let sequents_viewer = let new_proof (proof: MatitaTypes.proof) = let xmldump_observer _ _ = print_endline proof#toString in let proof_observer _ (status, ()) = - debug_print "proof_observer"; let ((uri_opt, _, _, _), _) = status in - let uri = MatitaTypes.unopt_uri uri_opt in - debug_print "apply transformation"; proof_viewer#load_proof status; - debug_print "/proof_observer" in let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) = sequents_viewer#reset; @@ -96,8 +89,10 @@ let new_proof (proof: MatitaTypes.proof) = sequents_observer); ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events proof_observer); +(* ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events xmldump_observer); +*) proof#notify; set_proof (Some proof) @@ -135,6 +130,43 @@ let ask_term ?(title = "term input") ?(msg = "insert term") () = Some term | None -> None +(** {2 Script window handling} *) + +let script_forward _ = + let buf = gui#script#scriptTextView#buffer in + let locked_iter = buf#get_iter_at_mark (`NAME "locked") in + interpreter#evalPhrase + (buf#get_text ~start:locked_iter ~stop:buf#end_iter ()); + gui#lockScript (locked_iter#offset + interpreter#endOffset) + +let script_jump _ = + let buf = gui#script#scriptTextView#buffer in + let locked_iter = buf#get_iter_at_mark (`NAME "locked") in + let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in + let raw_text = buf#get_text ~start:locked_iter ~stop:cursor_iter () in + let len = String.length raw_text in + let rec parse offset = + if offset < len then begin + interpreter#evalPhrase ~transparent:true + (String.sub raw_text offset (len - offset)); + let new_offset = interpreter#endOffset + offset in + gui#lockScript (new_offset + locked_iter#offset); + parse new_offset + end + in + try + parse 0 + with CicTextualParser2.Parse_error _ -> () + +let script_back _ = not_implemented "script_back" + +let load_script fname = + gui#script#scriptTextView#buffer#set_text (input_file fname); + gui#script#scriptWin#show (); + gui#main#showScriptMenuItem#set_active true + +(** {2 GUI callbacks} *) + let _ = gui#setQuitCallback quit; gui#setPhraseCallback interpreter#evalPhrase; @@ -156,14 +188,14 @@ let _ = ignore (gui#main#openMenuItem#connect#activate (fun _ -> match gui#chooseFile () with | None -> () - | Some f when is_proof_script f -> - gui#script#scriptTextView#buffer#set_text (input_file f); - gui#script#scriptWin#show (); - gui#main#showScriptMenuItem#set_active true + | Some f when is_proof_script f -> load_script f | Some f -> gui#console#echo_error (sprintf "Don't know what to do with file: %s\nUnrecognized file format." f))); + ignore (gui#script#scriptWinForwardButton#connect#clicked script_forward); + ignore (gui#script#scriptWinBackButton#connect#clicked script_back); + ignore (gui#script#scriptWinJumpButton#connect#clicked script_jump); let tac_w_term name tac _ = match ask_term ~title:name ~msg:("term for " ^ name) () with | Some term -> (get_proof ())#apply_tactic (tac ~term) @@ -235,5 +267,9 @@ let _ = (** *) -let _ = GtkThread.main () +let _ = + (try + load_script Sys.argv.(1) + with Invalid_argument _ -> ()); + GtkThread.main () diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 603a480f4..eb77ffa5d 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -165,8 +165,8 @@ class console buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props] (msg ^ "\n"); self#ignore_insert_text_signal false; - self#lock; - self#echo_prompt () + self#lock +(* self#echo_prompt () *) (** navigation methods: history, cursor motion, ... *) diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index 95ae9648e..a4423041f 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -544,10 +544,18 @@ class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata)) method vbox3 = vbox3 - val label6 = + val interpChoiceDialogLabel = new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label6" ~info:"GtkLabel" xmldata)) - method label6 = label6 + (Glade.get_widget_msg ~name:"InterpChoiceDialogLabel" ~info:"GtkLabel" xmldata)) + method interpChoiceDialogLabel = interpChoiceDialogLabel + val scrolledwindow4 = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast + (Glade.get_widget_msg ~name:"scrolledwindow4" ~info:"GtkScrolledWindow" xmldata)) + method scrolledwindow4 = scrolledwindow4 + val interpChoiceTreeView = + new GTree.view (GtkTree.TreeView.cast + (Glade.get_widget_msg ~name:"InterpChoiceTreeView" ~info:"GtkTreeView" xmldata)) + method interpChoiceTreeView = interpChoiceTreeView method reparent parent = dialog_vbox4#misc#reparent parent; toplevel#destroy () @@ -631,6 +639,10 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GBin.event_box (GtkBin.EventBox.cast (Glade.get_widget_msg ~name:"ScriptWinEventBox" ~info:"GtkEventBox" xmldata)) method scriptWinEventBox = scriptWinEventBox + val scriptNotebook = + new GPack.notebook (GtkPack.Notebook.cast + (Glade.get_widget_msg ~name:"scriptNotebook" ~info:"GtkNotebook" xmldata)) + method scriptNotebook = scriptNotebook val vbox4 = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"vbox4" ~info:"GtkVBox" xmldata)) @@ -639,26 +651,26 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GButton.toolbar (GtkButton.Toolbar.cast (Glade.get_widget_msg ~name:"toolbar1" ~info:"GtkToolbar" xmldata)) method toolbar1 = toolbar1 - val button5 = + val scriptWinBackButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"button5" ~info:"GtkButton" xmldata)) - method button5 = button5 + (Glade.get_widget_msg ~name:"ScriptWinBackButton" ~info:"GtkButton" xmldata)) + method scriptWinBackButton = scriptWinBackButton val image133 = new GMisc.image (GtkMisc.Image.cast (Glade.get_widget_msg ~name:"image133" ~info:"GtkImage" xmldata)) method image133 = image133 - val button6 = + val scriptWinJumpButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"button6" ~info:"GtkButton" xmldata)) - method button6 = button6 + (Glade.get_widget_msg ~name:"ScriptWinJumpButton" ~info:"GtkButton" xmldata)) + method scriptWinJumpButton = scriptWinJumpButton val image134 = new GMisc.image (GtkMisc.Image.cast (Glade.get_widget_msg ~name:"image134" ~info:"GtkImage" xmldata)) method image134 = image134 - val button7 = + val scriptWinForwardButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"button7" ~info:"GtkButton" xmldata)) - method button7 = button7 + (Glade.get_widget_msg ~name:"ScriptWinForwardButton" ~info:"GtkButton" xmldata)) + method scriptWinForwardButton = scriptWinForwardButton val image135 = new GMisc.image (GtkMisc.Image.cast (Glade.get_widget_msg ~name:"image135" ~info:"GtkImage" xmldata)) @@ -671,6 +683,22 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GText.view (GtkText.View.cast (Glade.get_widget_msg ~name:"ScriptTextView" ~info:"GtkTextView" xmldata)) method scriptTextView = scriptTextView + val label7 = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"label7" ~info:"GtkLabel" xmldata)) + method label7 = label7 + val scrolledwindow3 = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast + (Glade.get_widget_msg ~name:"scrolledwindow3" ~info:"GtkScrolledWindow" xmldata)) + method scrolledwindow3 = scrolledwindow3 + val treeview1 = + new GTree.view (GtkTree.TreeView.cast + (Glade.get_widget_msg ~name:"treeview1" ~info:"GtkTreeView" xmldata)) + method treeview1 = treeview1 + val label8 = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"label8" ~info:"GtkLabel" xmldata)) + method label8 = label8 method reparent parent = scriptWinEventBox#misc#reparent parent; toplevel#destroy () diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index d8e34fca3..28beebc27 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -315,9 +315,11 @@ class interpChoiceDialog : val dialog_vbox4 : GPack.box val interpChoiceCancelButton : GButton.button val interpChoiceDialog : GWindow.dialog_any + val interpChoiceDialogLabel : GMisc.label val interpChoiceHelpButton : GButton.button val interpChoiceOkButton : GButton.button - val label6 : GMisc.label + val interpChoiceTreeView : GTree.view + val scrolledwindow4 : GBin.scrolled_window val toplevel : GWindow.dialog_any val vbox3 : GPack.box val xml : Glade.glade_xml Gtk.obj @@ -327,10 +329,12 @@ class interpChoiceDialog : method dialog_vbox4 : GPack.box method interpChoiceCancelButton : GButton.button method interpChoiceDialog : GWindow.dialog_any + method interpChoiceDialogLabel : GMisc.label method interpChoiceHelpButton : GButton.button method interpChoiceOkButton : GButton.button - method label6 : GMisc.label + method interpChoiceTreeView : GTree.view method reparent : GObj.widget -> unit + method scrolledwindow4 : GBin.scrolled_window method toplevel : GWindow.dialog_any method vbox3 : GPack.box method xml : Glade.glade_xml Gtk.obj @@ -387,35 +391,45 @@ class scriptWin : ?autoconnect:bool -> unit -> object - val button5 : GButton.button - val button6 : GButton.button - val button7 : GButton.button val image133 : GMisc.image val image134 : GMisc.image val image135 : GMisc.image + val label7 : GMisc.label + val label8 : GMisc.label + val scriptNotebook : GPack.notebook val scriptTextView : GText.view val scriptWin : GWindow.window + val scriptWinBackButton : GButton.button val scriptWinEventBox : GBin.event_box + val scriptWinForwardButton : GButton.button + val scriptWinJumpButton : GButton.button val scrolledScript : GBin.scrolled_window + val scrolledwindow3 : GBin.scrolled_window val toolbar1 : GButton.toolbar val toplevel : GWindow.window + val treeview1 : GTree.view val vbox4 : GPack.box val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit - method button5 : GButton.button - method button6 : GButton.button - method button7 : GButton.button method check_widgets : unit -> unit method image133 : GMisc.image method image134 : GMisc.image method image135 : GMisc.image + method label7 : GMisc.label + method label8 : GMisc.label method reparent : GObj.widget -> unit + method scriptNotebook : GPack.notebook method scriptTextView : GText.view method scriptWin : GWindow.window + method scriptWinBackButton : GButton.button method scriptWinEventBox : GBin.event_box + method scriptWinForwardButton : GButton.button + method scriptWinJumpButton : GButton.button method scrolledScript : GBin.scrolled_window + method scrolledwindow3 : GBin.scrolled_window method toolbar1 : GButton.toolbar method toplevel : GWindow.window + method treeview1 : GTree.view method vbox4 : GPack.box method xml : Glade.glade_xml Gtk.obj end diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 2ff018a52..874c75c59 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -23,6 +23,10 @@ * http://helm.cs.unibo.it/ *) +open Printf + +open MatitaTypes + let toggle_visibility ~(win: GWindow.window) ~(check: GMenu.check_menu_item) = ignore (check#connect#toggled (fun _ -> if check#active then win#show () else win#misc#hide ())); @@ -75,6 +79,54 @@ class stringListModel (tree_view: GTree.view) = end +class interpModel = + let cols = new GTree.column_list in + let id_col = cols#add Gobject.Data.string in + let dsc_col = cols#add Gobject.Data.string in + let interp_no_col = cols#add Gobject.Data.int in + let tree_store = GTree.tree_store cols in + let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in + let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in + let id_view_col = GTree.view_column ~renderer:id_renderer () in + let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in + fun tree_view choices -> + object + initializer + tree_view#set_model (Some (tree_store :> GTree.model)); + ignore (tree_view#append_column id_view_col); + ignore (tree_view#append_column dsc_view_col); + let name_of_interp = + (* try to find a reasonable name for an interpretation *) + let idx = ref 0 in + fun interp -> + try + List.assoc "0" interp + with Not_found -> + incr idx; string_of_int !idx + in + tree_store#clear (); + let idx = ref ~-1 in + List.iter + (fun interp -> + incr idx; + let interp_row = tree_store#append () in + tree_store#set ~row:interp_row ~column:id_col + (name_of_interp interp); + tree_store#set ~row:interp_row ~column:interp_no_col !idx; + List.iter + (fun (id, dsc) -> + let row = tree_store#append ~parent:interp_row () in + tree_store#set ~row ~column:id_col id; + tree_store#set ~row ~column:dsc_col dsc; + tree_store#set ~row ~column:interp_no_col !idx) + interp) + choices + + method get_interp_no tree_path = + let iter = tree_store#get_iter tree_path in + tree_store#get ~row:iter ~column:interp_no_col + end + let is_var_uri s = try String.sub s (String.length s - 4) 4 = ".var" @@ -84,9 +136,10 @@ let non p x = not (p x) class type gui = object - method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog - method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog + method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end exception Cancel @@ -135,10 +188,34 @@ let interactive_user_uri_choice end let interactive_interp_choice ~(gui:#gui) choices = - (* TODO Zack implement interactive_interp_choice *) - MatitaTypes.warning - "'interactive_interp_choice' not implemented: returning 1st interpretation"; - [0] + assert (choices <> []); + let dialog = gui#newInterpDialog () in + let model = new interpModel dialog#interpChoiceTreeView choices in + let interp_len = List.length (List.hd choices) in + dialog#interpChoiceDialog#set_title "Interpretation choice"; + dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:"; + let interp_no = ref None in + let return _ = + dialog#interpChoiceDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true)); + ignore (dialog#interpChoiceOkButton#connect#clicked (fun _ -> + match !interp_no with None -> () | Some _ -> return ())); + ignore (dialog#interpChoiceCancelButton#connect#clicked return); + ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ -> + interp_no := Some (model#get_interp_no path); + return ())); + let selection = dialog#interpChoiceTreeView#selection in + ignore (selection#connect#changed (fun _ -> + match selection#get_selected_rows with + | [path] -> + debug_print (sprintf "selection: %d" (model#get_interp_no path)); + interp_no := Some (model#get_interp_no path) + | _ -> assert false)); + dialog#interpChoiceDialog#show (); + GtkThread.main (); + (match !interp_no with Some row -> [row] | _ -> raise Cancel) let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () = let dialog = gui#newConfirmationDialog () in diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index 8c45d4d59..fa12ab42e 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -50,9 +50,10 @@ class stringListModel: class type gui = object (* minimal gui object requirements *) - method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog - method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog + method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end (** {3 Dialogs} *) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index d50a2f319..9226ea7b6 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -64,9 +64,17 @@ class gui file = MatitaConsole.console ~evbox:main#consoleEventBox ~phrase_sep:";;" ~packing:main#scrolledConsole#add () in + let script_buf = script#scriptTextView#buffer in object (self) val mutable chosen_file = None + (** text mark and tag representing locked part of a script *) + val locked_mark = + script_buf#create_mark ~name:"locked" ~left_gravity:true + script_buf#start_iter + val locked_tag = + script_buf#create_tag [`BACKGROUND "green"; `EDITABLE false] + initializer (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) @@ -109,6 +117,7 @@ class gui file = | `CANCEL -> return None | `HELP -> () | `DELETE_EVENT -> return None)); + (* script *) (* menus *) List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem; main#saveAsMenuItem ]; @@ -184,6 +193,14 @@ class gui file = GtkThread.main (); !text + method lockScript offset = + let mark = `MARK locked_mark in + script_buf#move_mark mark ~where:(script_buf#get_iter_at_char offset); + script_buf#remove_tag locked_tag ~start:script_buf#start_iter + ~stop:script_buf#end_iter; + script_buf#apply_tag locked_tag ~start:script_buf#start_iter + ~stop:(script_buf#get_iter_at_mark mark) + end let instance = diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index a74403fdb..d3dc10a1d 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -62,9 +62,18 @@ class gui : method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog + (** {2 Utility methods} *) + + (** ask the used to choose a file with the file chooser *) method chooseFile: unit -> string option + + (** prompt the user for a (multiline) text entry *) method askText: ?title:string -> ?msg:string -> unit -> string option + (** lock script text view from the beginning to the given offset (in UTF-8 + * characters) *) + method lockScript: int -> unit + end (** singleton instance of the gui *) diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index d5ca65d22..35ec6119d 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -34,13 +34,25 @@ open Printf +open MatitaTypes + (** None means: "same state as before" *) type state_tag = [ `Command | `Proof ] option exception Command_error of string +(* let uri name = UriManager.uri_of_string (sprintf "%s/%s" BuildTimeConf.base_uri name) +*) + +let baseuri = ref "cic:/matita" +let qualify name = + let baseuri = !baseuri in + if baseuri.[String.length baseuri - 1] = '/' then + baseuri ^ name + else + String.concat "/" [baseuri; name] let canonical_context metano metasenv = try @@ -74,16 +86,49 @@ let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~proof_handler ast = end else disambiguator#disambiguateTermAst ast -class virtual interpreterState ~(console: MatitaConsole.console) = +class virtual interpreterState = + (* static values, shared by all states inheriting this class *) + let loc = ref None in + let history = ref [] in + fun ~(console: MatitaConsole.console) -> object (self) + (** eval a toplevel phrase in the current state and return the new state *) - method parsePhrase s = CicTextualParser2.parse_tactical (Stream.of_string s) + method parsePhrase s = + match CicTextualParser2.parse_tactical (Stream.of_string s) with + | (TacticAst.LocatedTactical (loc', tac)) as tactical -> + loc := Some loc'; + (match tac with (* update interpreter history *) + | TacticAst.Command (TacticAst.Qed None) -> + history := `Qed :: !history + | TacticAst.Command (TacticAst.Theorem (_, Some name, _, None)) -> + history := `Theorem name :: !history + | TacticAst.Command (TacticAst.Qed _) + | TacticAst.Command (TacticAst.Theorem _) -> assert false + | _ -> history := `Tactic :: !history); + tactical + | _ -> assert false method virtual evalTactical: (CicAst.term, string) TacticAst.tactical -> state_tag - method evalPhrase s = self#evalTactical (self#parsePhrase s) +(* + method undo ?(steps = 1) () = + for i = 1 to steps do + match List.hd !history with + | `Qed + FINQUI +*) + + method evalPhrase s = + debug_print (sprintf "evaluating '%s'" s); + self#evalTactical (self#parsePhrase s) + + method endOffset = + match !loc with + | Some (start_pos, end_pos) -> end_pos.Lexing.pos_cnum + | None -> failwith "MatitaInterpreter: no offset recorded" end @@ -108,6 +153,13 @@ class sharedState | TacticAst.Command TacticAst.Proof -> (* do nothing, just for compatibility with coq syntax *) Some `Command + | TacticAst.Command (TacticAst.Baseuri (Some uri)) -> + baseuri := uri; + console#echo_message (sprintf "base uri set to \"%s\"" uri); + None + | TacticAst.Command (TacticAst.Baseuri None) -> + console#echo_message (sprintf "base uri is \"%s\"" !baseuri); + None | TacticAst.Command (TacticAst.Check term) -> let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in let (context, metasenv) = get_context_and_metasenv proof_handler in @@ -138,14 +190,10 @@ class commandState method evalTactical = function | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical - | TacticAst.Command (TacticAst.Theorem (_, name_opt, ast, None)) -> + | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) -> let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in - let uri = - match name_opt with - | None -> None - | Some name -> Some (uri name) - in - let proof = MatitaProof.proof ~typ:expr ?uri ~metasenv () in + let uri = UriManager.uri_of_string (qualify name) in + let proof = MatitaProof.proof ~typ:expr ~uri ~metasenv () in proof_handler.MatitaTypes.new_proof proof; Some `Proof | TacticAst.Command TacticAst.Quit -> @@ -240,14 +288,11 @@ class proofState | TacticAst.Command (TacticAst.Redo steps) -> (proof_handler.MatitaTypes.get_proof ())#redo ?steps (); Some `Proof - | TacticAst.Command (TacticAst.Qed name_opt) -> + | TacticAst.Command (TacticAst.Qed None) -> (* TODO Zack this function probably should not simply fail with * Failure, but rather raise some more meaningful exception *) if not (proof_handler.MatitaTypes.has_proof ()) then assert false; let proof = proof_handler.MatitaTypes.get_proof () in - (match name_opt with - | None -> () - | Some name -> proof#set_uri (uri name)); let (uri, metasenv, bo, ty) = proof#proof in let uri = MatitaTypes.unopt_uri uri in if metasenv <> [] then failwith "Proof not completed"; @@ -258,6 +303,7 @@ class proofState CicEnvironment.add_type_checked_term uri (Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[])); proof_handler.MatitaTypes.set_proof None; + (MatitaMathView.proof_viewer_instance ())#unload; (* TODO Zack a lot more to be done here: * - save object to disk in xml format * - collect metadata @@ -289,34 +335,22 @@ class interpreter method reset = state <- commandState + method endOffset = state#endOffset + method private updateState = function | Some `Command -> state <- commandState | Some `Proof -> state <- proofState | None -> () - method evalPhrase s = + method evalPhrase ?(transparent = false) s = try self#updateState (state#evalPhrase s) with exn -> - console#echo_error (sprintf "Uncaught exception: %s" - (Printexc.to_string exn)) - -(* - method evalAll s = - let get_end_pos = function - | TacticAst.LocatedTactical ((_, end_pos), _) -> end_pos.Lexing.pos_cnum - | _ -> assert false - in - let str_len = String.length s in - let rec aux offset = - let tactical = - self#parsePhrase (String.sub s offset (str_len - offset)) - in - self#updateState (state#evalTactical tactical); - let next_offset = get_end_pos tactical + offset in - if next_offset = str_len - 1 then - in -*) + if transparent then + raise exn + else + console#echo_error (sprintf "Uncaught exception: %s" + (Printexc.to_string exn)) end diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 092362229..b83c9b37f 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -49,7 +49,8 @@ class proof_viewer obj = inherit GMathViewAux.single_selection_math_view obj -(* initializer self#set_log_verbosity 3 *) + val mutable current_infos = None + val mutable current_mathml = None initializer ignore (self#connect#click (fun (gdome_elt, _, _, _) -> @@ -57,10 +58,12 @@ class proof_viewer obj = | Some gdome_elt -> prerr_endline (gdome_elt#get_nodeName#to_string); ignore (self#action_toggle gdome_elt) - | None -> ())) - - val mutable current_infos = None - val mutable current_mathml = None + | None -> ())); + (* bugfix: until mapping gtkmathview doesn't draw anything *) + ignore (self#misc#connect#after#map (fun _ -> + match current_mathml with + | None -> () + | Some mathml -> self#load_root ~root:mathml#get_documentElement)) method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) = let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, @@ -77,12 +80,10 @@ class proof_viewer obj = ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/proof" ~doc:mathml ()); match current_mathml with | None -> - debug_print "no previous MathML"; self#load_root ~root:mathml#get_documentElement ; current_mathml <- Some mathml | Some current_mathml -> - debug_print "Previous MathML available: xmldiffing ..."; - self#freeze ; + self#freeze; XmlDiff.update_dom ~from:current_mathml mathml ; self#thaw end @@ -155,11 +156,15 @@ class sequent_viewer obj = class sequents_viewer ~(notebook:GPack.notebook) ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal () = + let tab_label metano = + (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce + in object (self) val mutable pages = 0 val mutable switch_page_callback = None val mutable page2goal = [] (* associative list: page no -> goal no *) val mutable goal2page = [] (* the other way round *) + val mutable goal2win = [] (* associative list: goal no -> scrolled win *) val mutable _metasenv = [] method reset = @@ -167,6 +172,7 @@ class sequents_viewer ~(notebook:GPack.notebook) pages <- 0; page2goal <- []; goal2page <- []; + goal2win <- []; _metasenv <- []; (match switch_page_callback with | Some id -> @@ -177,35 +183,43 @@ class sequents_viewer ~(notebook:GPack.notebook) method load_sequents metasenv = let sequents_no = List.length metasenv in _metasenv <- metasenv; - debug_print (sprintf "sequents no: %d" sequents_no); pages <- sequents_no; - let widget = sequent_viewer#coerce in + let win metano = + let w = + GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC + ~show:true () + in + let reparent () = + match sequent_viewer#misc#parent with + | None -> w#add sequent_viewer#coerce + | Some _ -> sequent_viewer#misc#reparent w#coerce + in + goal2win <- (metano, reparent) :: goal2win; + w#coerce + in let page = ref 0 in List.iter (fun (metano, _, _) -> page2goal <- (!page, metano) :: page2goal; goal2page <- (metano, !page) :: goal2page; incr page; - let tab_label = - (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce - in - notebook#append_page ~tab_label widget) + notebook#append_page ~tab_label:(tab_label metano) (win metano)) metasenv; switch_page_callback <- - (* TODO Zack the "#after" may probably be removed after Luca's fix for - * widget not loading documents before being realized *) Some (notebook#connect#after#switch_page ~callback:(fun page -> - debug_print "switch_page callback"; let goal = try List.assoc page page2goal with Not_found -> assert false in set_goal goal; - self#render_page goal)) + self#render_page ~page ~goal)) - method private render_page goal = - sequent_viewer#load_sequent _metasenv goal + method private render_page ~page ~goal = + sequent_viewer#load_sequent _metasenv goal; + try + List.assoc goal goal2win () + with Not_found -> assert false method goto_sequent goal = let page = @@ -214,7 +228,7 @@ class sequents_viewer ~(notebook:GPack.notebook) with Not_found -> assert false in notebook#goto_page page; - self#render_page goal + self#render_page page goal end @@ -236,6 +250,17 @@ let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = ~font_size ~log_verbosity)) [] +let proof_viewer_instance = + let instance = lazy ( + let gui = MatitaGui.instance () in + let frame = + GBin.frame ~packing:(gui#proof#scrolledProof#add_with_viewport) + ~show:true () + in + proof_viewer ~show:true ~packing:(frame#add) () + ) in + fun () -> Lazy.force instance + let sequents_viewer ~(notebook:GPack.notebook) ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal () = diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index b0ceda45c..02141cde5 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -35,6 +35,10 @@ val proof_viewer: unit -> MatitaTypes.proof_viewer + (** singleton proof_viewer instance. + * Uses singleton GUI instance *) +val proof_viewer_instance: unit -> MatitaTypes.proof_viewer + val sequent_viewer: ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index bea4377e6..20ffd350d 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -35,6 +35,9 @@ let debug_print s = exception No_proof (** no current proof is available *) +exception Cancel + +(* let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con" let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind" @@ -42,6 +45,8 @@ let unopt_uri ?(kind = `Con) = function | Some uri -> uri | None -> (match kind with `Con -> untitled_con_uri | `Def -> untitled_def_uri) +*) +let unopt_uri = function Some uri -> uri | None -> assert false class type parserr = (* "parser" is a keyword :-( *) object @@ -123,17 +128,24 @@ class type interpreter = method reset: unit (** return the interpreter to the initial state *) (** parse a single phrase contained in the input string. Additional - * garbage at the end of the phrase is ignored *) - method evalPhrase: string -> unit + * garbage at the end of the phrase is ignored + * @param transparent per default the interpreter catch all exceptions ans + * prints them in the console. When transparent is set to true exceptions + * are flow through. Defaults to false + *) + method evalPhrase: ?transparent:bool -> string -> unit + + (** offset from the starting of the last string parser by evalPhrase where + * parsing stop. + * @raise Failure when no offset has been recorded *) + method endOffset: int (* - (** eval zero or more phrases contained in the input string. Additional - * garbage contained at the end of the last phrase is ignored. - * @return offset from the beginning of the string pointing to the end of - * the last parsed phrase. Next invocations of evalAll should start from - * there *) - method evalAll: string -> int + (** undo last steps phrases. + * @param steps number of phrases to undo; defaults to 1 *) + method undo: ?steps:int -> unit -> unit *) + end (** {2 MathML widgets} *)