From: Stefano Zacchiroli Date: Mon, 4 Oct 2004 09:31:15 +0000 (+0000) Subject: snapshot X-Git-Tag: V_0_0_10~106 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1fa0472bfe2ed04c7adf166fa48df687f0022226;p=helm.git snapshot --- diff --git a/helm/matita/.depend b/helm/matita/.depend index 0034c0c4a..a21785af7 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,17 +1,15 @@ -logicalOperations.cmo: logicalOperations.cmi -logicalOperations.cmx: logicalOperations.cmi -matitaConsole.cmo: matitaConsole.cmi -matitaConsole.cmx: matitaConsole.cmi +matitaConsole.cmo: matitaGtkMisc.cmi matitaConsole.cmi +matitaConsole.cmx: matitaGtkMisc.cmx matitaConsole.cmi matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi matitaGeneratedGui.cmx: matitaGeneratedGui.cmi matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaTypes.cmo matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaTypes.cmx matitaGtkMisc.cmi -matitaGui.cmo: matitaConsole.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi \ - matitaGui.cmi -matitaGui.cmx: matitaConsole.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmx \ - matitaGui.cmi +matitaGui.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGeneratedGui.cmi \ + matitaGtkMisc.cmi matitaGui.cmi +matitaGui.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGeneratedGui.cmx \ + matitaGtkMisc.cmx matitaGui.cmi matitaInterpreter.cmo: matitaConsole.cmi matitaProof.cmi matitaTypes.cmo \ matitaInterpreter.cmi matitaInterpreter.cmx: matitaConsole.cmx matitaProof.cmx matitaTypes.cmx \ @@ -19,14 +17,15 @@ matitaInterpreter.cmx: matitaConsole.cmx matitaProof.cmx matitaTypes.cmx \ matitaMathView.cmo: matitaTypes.cmo matitaMathView.cmi matitaMathView.cmx: matitaTypes.cmx matitaMathView.cmi matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \ - matitaGui.cmi matitaInterpreter.cmi matitaProof.cmi matitaTypes.cmo + matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi matitaProof.cmi \ + matitaTypes.cmo matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \ - matitaGui.cmx matitaInterpreter.cmx matitaProof.cmx matitaTypes.cmx -matitaProof.cmo: matitaTypes.cmo matitaProof.cmi -matitaProof.cmx: matitaTypes.cmx matitaProof.cmi + matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx matitaProof.cmx \ + matitaTypes.cmx +matitaProof.cmo: buildTimeConf.cmo matitaTypes.cmo matitaProof.cmi +matitaProof.cmx: buildTimeConf.cmx matitaTypes.cmx matitaProof.cmi matitaTypes.cmo: buildTimeConf.cmo matitaTypes.cmx: buildTimeConf.cmx -logicalOperations.cmi: matitaTypes.cmo matitaDisambiguator.cmi: matitaTypes.cmo matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaTypes.cmo matitaGui.cmi: matitaConsole.cmi matitaGeneratedGui.cmi diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index 665bb4908..4f2a4d27c 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -24,6 +24,6 @@ *) let debug = @DEBUG@;; - -module Transformer = @TRANSFORMER_MODULE@;; +let version = "0.0.1";; +let history_size = 10;; diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 0602d067d..c29718dbf 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -29,6 +29,7 @@ fi FINDLIB_REQUIRES="\ lablgtk2.glade \ +lablgtk2.init \ lablgtkmathview \ pcre \ helm-cic_omdoc \ @@ -82,8 +83,6 @@ if test "$DEBUG" = "true"; then echo "debugging enabled" fi -TRANSFORMER_MODULE=ApplyTransformation - AC_SUBST(CAMLP4O) AC_SUBST(DEBUG) AC_SUBST(TRANSFORMER_MODULE) diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index 7df0d1961..ae7b7a430 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -7,8 +7,8 @@
mathql_db_map.txt
- mowgli.cs.unibo.it - + + localhost mowgli @@ -29,7 +29,7 @@
remote - http://mowgli.cs.unibo.it:58081/ - + + http://localhost:58081/
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 07c46bd4b..c793a2bc8 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -20,305 +20,335 @@ GDK_GRAVITY_NORTH_WEST - + True - False - 0 + True + False - + True + False + 0 - + True - _File - True - + + True + _File + True - - True - _New - True + - - + + True - gtk-new - 1 - 0.5 - 0.5 - 0 - 0 + _New + True + + + + True + gtk-new + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + + True + _Proof or definition ... + True + + + + + + True + (Co)Inductive _definitions ... + True + + + + - + + True + _Open... + True + - - + + True - _Proof or definition ... - True - + gtk-open + 1 + 0.5 + 0.5 + 0 + 0 + + - - + + + True + _Save + True + + + + True - (Co)Inductive _definitions ... - True + gtk-save + 1 + 0.5 + 0.5 + 0 + 0 - - - - - - True - _Open... - True - - - + + True - gtk-open - 1 - 0.5 - 0.5 - 0 - 0 + Save _As ... + True + + + + True + gtk-save-as + 1 + 0.5 + 0.5 + 0 + 0 + + - - - - - True - _Save - True - + + + True + + - - + + True - gtk-save - 1 - 0.5 - 0.5 - 0 - 0 + _Quit + True + + + + + True + gtk-quit + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + _Edit + True + + + + + + True + _View + True - - True - Save _As ... - True + - - + + True - gtk-save-as - 1 - 0.5 - 0.5 - 0 - 0 + Show Button Bar + True + True - - - - - True + + + True + Show Proof Window + True + False + + + + + + + + + True + Debug + True - - True - _Quit - True - + - - + + True - gtk-quit - 1 - 0.5 - 0.5 - 0 - 0 - - - - - - True - _Edit - True - - - - - - True - _View - True - + + True + _Help + True - - True - Show Button Bar - True - True - - + - - - True - Show Proof Window - True - False - + + + True + About... + True + + + + 0 + False + False + - + True - Debug - True + True + 450 - + + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT - + True + GTK_SHADOW_IN + + + + True + True + True + True + GTK_POS_TOP + False + False + + + + True + False + - - - - - - True - _Help - True - + + True + True + False - + True - About... - True + GTK_POLICY_NEVER + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + - - - - - - 0 - False - False - - - - - - True - True - 450 - - - - True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT - - - + + True + True + - True - False + 0 + True + True - + True - GTK_POLICY_NEVER - GTK_POLICY_ALWAYS - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - - - - + True - True - True + 0 + False + False - - 0 - True - True - - - - - - True - True - - - 0 - False - False - @@ -638,7 +668,29 @@ - + + True + <b>Matita @VERSION@</b> + +<tt>http://helm.cs.unibo.it</tt> + +Copyright (C) 2004, +<i>the HELM team</i> + False + True + GTK_JUSTIFY_CENTER + False + False + 0.5 + 0.5 + 5 + 5 + + + 0 + False + False + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 3c543d5c1..28dee4947 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -23,20 +23,22 @@ * http://helm.cs.unibo.it/ *) +open Printf + open MatitaGtkMisc (** {2 Internal status} *) let (get_proof, set_proof, has_proof) = let (current_proof: MatitaTypes.proof option ref) = ref None in - ((fun () -> + ((fun () -> (* get_proof *) match !current_proof with | Some proof -> proof | None -> failwith "No current proof"), - (fun proof -> (* TODO Zack: this function should probably be smarter taking - care also of unregistering notifications subscriber and so on *) - current_proof := proof), - (fun () -> !current_proof <> None)) + (fun proof -> (* set_proof *) + current_proof := proof), + (fun () -> (* has_proof *) + !current_proof <> None)) (** {2 Settings} *) @@ -61,46 +63,99 @@ let disambiguator = ~chooseInterp:(interactive_interp_choice ~gui) () let proof_viewer = - let mml_of_cic_object = BuildTimeConf.Transformer.mml_of_cic_object in -(* let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) () -*) - MatitaMathView.proof_viewer ~show:true ~packing:(gui#proof#scrolledProof#add) () -(* -let sequent_viewer = - let mml_of_cic_sequent = BuildTimeConf.Transformer.mml_of_cic_sequent in - MatitaMathView.sequent_viewer ~mml_of_cic_sequent ~show:true - ~packing:(gui#main#scrolledSequents#add) () -*) +let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () let new_proof (proof: MatitaTypes.proof) = - (* TODO Zack a lot: - * - ids_to_inner_types, ids_to_inner_sorts handling - * - sequent viewer notification - *) let xmldump_observer _ _ = print_endline proof#toString in let proof_observer _ (status, metadata) = debug_print "proof_observer"; let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = - metadata + (fst metadata) in let ((uri_opt, _, _, _), _) = status in let uri = MatitaTypes.unopt_uri uri_opt in debug_print "apply transformation"; let mathml = - BuildTimeConf.Transformer.mml_of_cic_object + ApplyTransformation.mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types in if BuildTimeConf.debug then save_dom ~doc:mathml ~dest:"/tmp/matita.xml"; proof_viewer#load_proof mathml metadata; debug_print "/proof_observer" in + let sequents_observer = + let pages = ref 0 in + let callback_id = ref None in + let mathmls = ref [] in + fun _ ((proof, goal_opt) as status, metadata) -> + debug_print "sequents_observer"; + let notebook = gui#main#sequentsNotebook in + for i = 1 to !pages do + notebook#remove_page 0 + done; + mathmls := []; + (match !callback_id with + | Some id -> GtkSignal.disconnect notebook#as_widget id + | None -> ()); + if goal_opt <> None then begin + let sequents = snd metadata in + let sequents_no = List.length sequents in + debug_print (sprintf "sequents no: %d" sequents_no); + pages := sequents_no; + let widget = sequent_viewer#coerce in + List.iter + (fun (metano, (asequent, _, _, ids_to_inner_sorts, _)) -> + let tab_label = + (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce + in + notebook#append_page ~tab_label widget; + let mathml = lazy + (let content_sequent = Cic2content.map_sequent asequent in + let pres_sequent = + Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent + in + let xmlpres = Box.document_of_box pres_sequent in + Xml2Gdome.document_of_xml Misc.domImpl xmlpres) + in + mathmls := (metano, mathml) :: !mathmls) + sequents; + mathmls := List.rev !mathmls; + let render_page page = + let (metano, mathml) = List.nth !mathmls page in + sequent_viewer#load_sequent (Lazy.force mathml) metadata metano + in + callback_id := + (* 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"; + render_page page)); + (match goal_opt with + | Some goal -> (* current goal available, go to corresponding page *) + let page = ref 0 in + (try + List.iter + (fun (metano, _) -> + if (metano = goal) then raise Exit; + incr page) + sequents; + with Exit -> + debug_print (sprintf "going to page %d" !page); + notebook#goto_page !page; + render_page !page) + | None -> ()); + end; + debug_print "/sequents_observer" + in ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events - xmldump_observer); + 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) @@ -111,9 +166,12 @@ let quit () = (* quit program, asking for confirmation if needed *) then GMain.Main.quit () +let abort_proof () = + MatitaTypes.not_implemented "Matita.abort_proof" + let proof_handler = { MatitaTypes.get_proof = get_proof; - MatitaTypes.set_proof = set_proof; + MatitaTypes.abort_proof = abort_proof; MatitaTypes.has_proof = has_proof; MatitaTypes.new_proof = new_proof; MatitaTypes.quit = quit; diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 9c3c5a9b5..1f86e51a0 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -35,10 +35,37 @@ let prompt_props = [ ] let trailing_NL_RE = Pcre.regexp "\n\\s*$" +exception History_failure + + (** shell like phrase history *) +class history size = + let size = size + 1 in + let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in + let incr x = (x + 1) mod size in + object + val data = Array.create size "" + val mutable hd = 0 (* insertion point *) + val mutable tl = -1 (* oldest inserted item *) + val mutable cur = -1 (* current item for the history *) + method add s = + data.(hd) <- s; + if tl = -1 then tl <- hd; + hd <- incr hd; + if hd = tl then tl <- incr tl; + cur <- hd + method previous = + if cur = tl then raise History_failure; + cur <- decr cur; + data.(cur) + method next = + if cur = hd then raise History_failure; + cur <- incr cur; + if cur = hd then "" else data.(cur) + end + class console ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) - ?(callback = default_callback) - obj + ?(callback = default_callback) ?evbox obj = object (self) inherit GText.view obj @@ -47,6 +74,10 @@ class console method phrase_sep = _phrase_sep method set_phrase_sep sep = _phrase_sep <- sep + val mutable _prompt = prompt + method prompt = _prompt + method set_prompt prompt = _prompt <- prompt + val mutable _callback = callback method set_callback f = _callback <- f @@ -54,14 +85,7 @@ class console method ignore_insert_text_signal ignore = _ignore_insert_text_signal <- ignore -(* - (* TODO Zack: implement history. - IDEA: use CTRL-P/N a la emacs. - ISSUE: per-phrase or per-line history? *) - val phrases_history = Array.create history_size None - val mutable history_last_index = -1 - val mutable history_cur_index = -1 -*) + val history = new history history_size initializer let buf = self#buffer in @@ -83,9 +107,33 @@ class console let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *) self#lock; - _callback inserted_text; + self#invoke_callback inserted_text; self#echo_prompt () - end)) + end)); + (match evbox with + | None -> () + | Some evbox -> + List.iter (fun (key, f) -> MatitaGtkMisc.add_key_binding key f evbox) + [ GdkKeysyms._p, (fun () -> self#previous_phrase); + GdkKeysyms._n, (fun () -> self#next_phrase); + GdkKeysyms._a, (fun () -> self#beginning_of_phrase); + GdkKeysyms._e, (fun () -> self#end_of_phrase); + GdkKeysyms._f, (fun () -> self#forward_char); + GdkKeysyms._b, (fun () -> self#backward_char); + ]) + + method private set_phrase phrase = + let buf = self#buffer in + buf#delete + ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) + ~stop:buf#end_iter; + buf#insert ~iter:buf#end_iter phrase + + method private invoke_callback phrase = + history#add (* do not push trailing phrase separator *) + (String.sub phrase 0 + (String.length phrase - String.length _phrase_sep)); + _callback phrase (* lock old text and bump USER_INPUT_START mark *) method private lock = @@ -116,11 +164,31 @@ class console (msg ^ "\n"); self#ignore_insert_text_signal false; self#lock + + (** navigation methods: history, cursor motion, ... *) + + method private previous_phrase = + try self#set_phrase history#previous with History_failure -> () + method private next_phrase = + try self#set_phrase history#next with History_failure -> () + method private beginning_of_phrase = + let buf = self#buffer in + buf#place_cursor ~where:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) + method private end_of_phrase = + let buf = self#buffer in + buf#place_cursor ~where:buf#end_iter + method private forward_char = + let buf = self#buffer in + buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#forward_char + method private backward_char = + let buf = self#buffer in + buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#backward_char + end let console ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) - ?(callback = default_callback) + ?(callback = default_callback) ?evbox ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () = @@ -129,5 +197,5 @@ let console ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () in - new console ~prompt ~phrase_sep ~callback view#as_view + new console ~prompt ~phrase_sep ~callback ?evbox view#as_view diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli index 2cbd1ffe3..950776135 100644 --- a/helm/matita/matitaConsole.mli +++ b/helm/matita/matitaConsole.mli @@ -23,9 +23,11 @@ * http://helm.cs.unibo.it/ *) + (** @param evbox event box to which keyboard shortcuts are registered; no + * shortcut will be registered if evbox is not given *) class console: ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> unit) -> - Gtk.text_view Gtk.obj -> + ?evbox:GBin.event_box -> Gtk.text_view Gtk.obj -> object inherit GText.view @@ -33,6 +35,9 @@ class console: method echo_message : string -> unit method echo_error : string -> unit + method prompt : string + method set_prompt : string -> unit + method phrase_sep : string method set_phrase_sep : string -> unit @@ -51,6 +56,7 @@ val console : ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> unit) -> + ?evbox:GBin.event_box -> ?buffer:GText.buffer -> ?editable:bool -> diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index 09ecc1c57..9985ef086 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -12,6 +12,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GWindow.window (GtkWindow.Window.cast (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata)) method mainWin = mainWin + val mainWinEventBox = + new GBin.event_box (GtkBin.EventBox.cast + (Glade.get_widget_msg ~name:"MainWinEventBox" ~info:"GtkEventBox" xmldata)) + method mainWinEventBox = mainWinEventBox val mainWinShape = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"MainWinShape" ~info:"GtkVBox" xmldata)) @@ -32,10 +36,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata)) method newMenu = newMenu - val image76 = + val image84 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image76" ~info:"GtkImage" xmldata)) - method image76 = image76 + (Glade.get_widget_msg ~name:"image84" ~info:"GtkImage" xmldata)) + method image84 = image84 val newMenu_menu = new GMenu.menu (GtkMenu.Menu.cast (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata)) @@ -52,38 +56,38 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata)) method openMenuItem = openMenuItem - val image77 = + val image85 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image77" ~info:"GtkImage" xmldata)) - method image77 = image77 + (Glade.get_widget_msg ~name:"image85" ~info:"GtkImage" xmldata)) + method image85 = image85 val saveMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveMenuItem = saveMenuItem - val image78 = + val image86 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image78" ~info:"GtkImage" xmldata)) - method image78 = image78 + (Glade.get_widget_msg ~name:"image86" ~info:"GtkImage" xmldata)) + method image86 = image86 val saveAsMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveAsMenuItem = saveAsMenuItem - val image79 = + val image87 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image79" ~info:"GtkImage" xmldata)) - method image79 = image79 + (Glade.get_widget_msg ~name:"image87" ~info:"GtkImage" xmldata)) + method image87 = image87 val separator1 = new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"separator1" ~info:"GtkMenuItem" xmldata)) + (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata)) method separator1 = separator1 val quitMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata)) method quitMenuItem = quitMenuItem - val image80 = + val image88 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image80" ~info:"GtkImage" xmldata)) - method image80 = image80 + (Glade.get_widget_msg ~name:"image88" ~info:"GtkImage" xmldata)) + method image88 = image88 val editMenu = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata)) @@ -114,7 +118,7 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = method debugMenu_menu = debugMenu_menu val separator2 = new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"separator2" ~info:"GtkMenuItem" xmldata)) + (Glade.get_widget_msg ~name:"separator2" ~info:"GtkSeparatorMenuItem" xmldata)) method separator2 = separator2 val helpMenu = new GMenu.menu_item (GtkMenu.MenuItem.cast @@ -136,6 +140,18 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (Glade.get_widget_msg ~name:"ScrolledSequents" ~info:"GtkScrolledWindow" xmldata)) method scrolledSequents = scrolledSequents + val viewport1 = + new GBin.viewport (GtkBin.Viewport.cast + (Glade.get_widget_msg ~name:"viewport1" ~info:"GtkViewport" xmldata)) + method viewport1 = viewport1 + val sequentsNotebook = + new GPack.notebook (GtkPack.Notebook.cast + (Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata)) + method sequentsNotebook = sequentsNotebook + val consoleEventBox = + new GBin.event_box (GtkBin.EventBox.cast + (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata)) + method consoleEventBox = consoleEventBox val scrolledConsole = new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata)) @@ -145,7 +161,7 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata)) method mainStatusBar = mainStatusBar method reparent parent = - mainWinShape#misc#reparent parent; + mainWinEventBox#misc#reparent parent; toplevel#destroy () method check_widgets () = () end @@ -302,6 +318,10 @@ class aboutWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"AboutDismissButton" ~info:"GtkButton" xmldata)) method aboutDismissButton = aboutDismissButton + val aboutLabel = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"AboutLabel" ~info:"GtkLabel" xmldata)) + method aboutLabel = aboutLabel method reparent parent = dialog_vbox2#misc#reparent parent; toplevel#destroy () diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 2889d9279..5a383eb97 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -5,6 +5,7 @@ class mainWin : unit -> object val aboutMenuItem : GMenu.menu_item + val consoleEventBox : GBin.event_box val debugMenu : GMenu.menu_item val debugMenu_menu : GMenu.menu val editMenu : GMenu.menu_item @@ -12,15 +13,16 @@ class mainWin : val fileMenu_menu : GMenu.menu val helpMenu : GMenu.menu_item val helpMenu_menu : GMenu.menu - val image76 : GMisc.image - val image77 : GMisc.image - val image78 : GMisc.image - val image79 : GMisc.image - val image80 : GMisc.image + val image84 : GMisc.image + val image85 : GMisc.image + val image86 : GMisc.image + val image87 : GMisc.image + val image88 : GMisc.image val mainMenuBar : GMenu.menu_shell val mainStatusBar : GMisc.statusbar val mainVPanes : GPack.paned val mainWin : GWindow.window + val mainWinEventBox : GBin.event_box val mainWinShape : GPack.box val newDefsMenuItem : GMenu.menu_item val newMenu : GMenu.image_menu_item @@ -34,15 +36,18 @@ class mainWin : val scrolledSequents : GBin.scrolled_window val separator1 : GMenu.menu_item val separator2 : GMenu.menu_item + val sequentsNotebook : GPack.notebook val showProofMenuItem : GMenu.check_menu_item val showToolBarMenuItem : GMenu.check_menu_item val toplevel : GWindow.window val viewMenu : GMenu.menu_item val viewMenu_menu : GMenu.menu + val viewport1 : GBin.viewport val xml : Glade.glade_xml Gtk.obj method aboutMenuItem : GMenu.menu_item method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit + method consoleEventBox : GBin.event_box method debugMenu : GMenu.menu_item method debugMenu_menu : GMenu.menu method editMenu : GMenu.menu_item @@ -50,15 +55,16 @@ class mainWin : method fileMenu_menu : GMenu.menu method helpMenu : GMenu.menu_item method helpMenu_menu : GMenu.menu - method image76 : GMisc.image - method image77 : GMisc.image - method image78 : GMisc.image - method image79 : GMisc.image - method image80 : GMisc.image + method image84 : GMisc.image + method image85 : GMisc.image + method image86 : GMisc.image + method image87 : GMisc.image + method image88 : GMisc.image method mainMenuBar : GMenu.menu_shell method mainStatusBar : GMisc.statusbar method mainVPanes : GPack.paned method mainWin : GWindow.window + method mainWinEventBox : GBin.event_box method mainWinShape : GPack.box method newDefsMenuItem : GMenu.menu_item method newMenu : GMenu.image_menu_item @@ -73,11 +79,13 @@ class mainWin : method scrolledSequents : GBin.scrolled_window method separator1 : GMenu.menu_item method separator2 : GMenu.menu_item + method sequentsNotebook : GPack.notebook method showProofMenuItem : GMenu.check_menu_item method showToolBarMenuItem : GMenu.check_menu_item method toplevel : GWindow.window method viewMenu : GMenu.menu_item method viewMenu_menu : GMenu.menu + method viewport1 : GBin.viewport method xml : Glade.glade_xml Gtk.obj end class proofWin : @@ -182,12 +190,14 @@ class aboutWin : unit -> object val aboutDismissButton : GButton.button + val aboutLabel : GMisc.label val aboutWin : GWindow.dialog_any val dialog_action_area2 : GPack.button_box val dialog_vbox2 : GPack.box val toplevel : GWindow.dialog_any val xml : Glade.glade_xml Gtk.obj method aboutDismissButton : GButton.button + method aboutLabel : GMisc.label method aboutWin : GWindow.dialog_any method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 2018d7176..e3652a264 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -41,6 +41,8 @@ class stringListModel' uriChoiceDialog = end *) +open Printf + open MatitaGeneratedGui open MatitaGtkMisc @@ -52,9 +54,12 @@ class gui file = let fileSel = new fileSelectionWin ~file () in let proof = new proofWin ~file () in let keyBindingBoxes = (* event boxes which should receive global key events *) - [ toolbar#toolBarEventBox; proof#proofWinEventBox ] + [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox ] + in + let console = + MatitaConsole.console ~evbox:main#consoleEventBox + ~packing:main#scrolledConsole#add () in - let console = MatitaConsole.console ~packing:main#scrolledConsole#add () in object (self) initializer (* glade's check widgets *) @@ -75,12 +80,15 @@ class gui file = about#aboutWin#show ())); ignore (about#aboutDismissButton#connect#clicked (fun _ -> about#aboutWin#misc#hide ())); + about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@" + ~templ:BuildTimeConf.version about#aboutLabel#label); (* menus *) List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem; main#saveAsMenuItem ]; main#helpMenu#set_right_justified true; (* console *) - console#echo_message "\tMatita version 0.0.1\n"; + console#echo_message (sprintf "\tMatita version %s\n" + BuildTimeConf.version); console#echo_prompt (); console#misc#grab_focus () diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 6eb43600c..2f475f748 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -97,57 +97,26 @@ class commandState | tactical -> shared#evalTactical tactical end -let rec lookup_tactic = function - | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic - | TacticAst.Intros (_, names) -> - let namer = - (** use names given by the user as long as they are availble, then - * fallback on default fresh name generator *) - let len = List.length names in - let count = ref 0 in - fun metasenv context name ~typ -> - if !count < len then begin - let name = Cic.Name (List.nth names !count) in - incr count; - name - end else - FreshNamesGenerator.mk_fresh_name metasenv context name ~typ - in - PrimitiveTactics.intros_tac ~mk_fresh_name_callback:namer () - | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac - | TacticAst.Assumption -> VariousTactics.assumption_tac - | TacticAst.Contradiction -> NegationTactics.contradiction_tac - | TacticAst.Exists -> IntroductionTactics.exists_tac - | TacticAst.Fourier -> FourierR.fourier_tac - | TacticAst.Left -> IntroductionTactics.left_tac - | TacticAst.Right -> IntroductionTactics.right_tac - | TacticAst.Ring -> Ring.ring_tac - | TacticAst.Split -> IntroductionTactics.split_tac - | TacticAst.Symmetry -> EqualityTactics.symmetry_tac -(* - (* TODO Zack a lot more of tactics to be implemented here ... *) - | TacticAst.Absurd - | TacticAst.Apply of 'term - | TacticAst.Change of 'term * 'term * 'ident option - | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option - | TacticAst.Cut of 'term - | TacticAst.Decompose of 'ident * 'ident list - | TacticAst.Discriminate of 'ident - | TacticAst.Elim of 'term * 'term option - | TacticAst.ElimType of 'term - | TacticAst.Exact of 'term - | TacticAst.Fold of reduction_kind * 'term - | TacticAst.Injection of 'ident - | TacticAst.Intros of int option * 'ident list - | TacticAst.LetIn of 'term * 'ident - | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option - | TacticAst.Replace of 'term * 'term - | TacticAst.Replace_pattern of 'term pattern * 'term - | TacticAst.Rewrite of direction * 'term * 'ident option - | TacticAst.Transitivity of 'term -*) - | _ -> - MatitaTypes.not_implemented "some tactic" +let canonical_context metano metasenv = + try + let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in + context + with Not_found -> + failwith (sprintf "Can't find canonical context for %d" metano) + + (** create a ProofEngineTypes.mk_fresh_name_type function which uses given + * names as long as they are available, then it fallbacks to name generation + * using FreshNamesGenerator module *) +let namer_of names = + let len = List.length names in + let count = ref 0 in + fun metasenv context name ~typ -> + if !count < len then begin + let name = Cic.Name (List.nth names !count) in + incr count; + name + end else + FreshNamesGenerator.mk_fresh_name metasenv context name ~typ (** Implements phrases that should be accepted only in `Proof state, basically * tacticals *) @@ -157,6 +126,62 @@ class proofState ~(console: MatitaConsole.console) () = + (** term AST -> Cic.term. Uses disambiguator and change imperatively the + * metasenv as needed *) + let disambiguate ast = + let proof = proof_handler.MatitaTypes.get_proof () in + let metasenv = proof#metasenv in + let goal = proof#goal in + let context = canonical_context goal metasenv in + let (_, metasenv, term) = + disambiguator#disambiguateTermAst ~context ~metasenv ast + in + proof#set_metasenv metasenv; + term + in + (** tactic AST -> ProofEngineTypes.tactic *) + let rec lookup_tactic = function + | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic + | TacticAst.Intros (_, names) -> (* TODO Zack implement intros length *) + PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () + | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac + | TacticAst.Assumption -> VariousTactics.assumption_tac + | TacticAst.Contradiction -> NegationTactics.contradiction_tac + | TacticAst.Exists -> IntroductionTactics.exists_tac + | TacticAst.Fourier -> FourierR.fourier_tac + | TacticAst.Left -> IntroductionTactics.left_tac + | TacticAst.Right -> IntroductionTactics.right_tac + | TacticAst.Ring -> Ring.ring_tac + | TacticAst.Split -> IntroductionTactics.split_tac + | TacticAst.Symmetry -> EqualityTactics.symmetry_tac + | TacticAst.Transitivity term -> + EqualityTactics.transitivity_tac (disambiguate term) + | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term) + | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term) + | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term) + | TacticAst.ElimType term -> + EliminationTactics.elim_type_tac (disambiguate term) + | TacticAst.Replace (what, with_what) -> + EqualityTactics.replace_tac ~what:(disambiguate what) + ~with_what:(disambiguate with_what) + (* + (* TODO Zack a lot more of tactics to be implemented here ... *) + | TacticAst.Absurd + | TacticAst.Change of 'term * 'term * 'ident option + | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option + | TacticAst.Decompose of 'ident * 'ident list + | TacticAst.Discriminate of 'ident + | TacticAst.Elim of 'term * 'term option + | TacticAst.Fold of reduction_kind * 'term + | TacticAst.Injection of 'ident + | TacticAst.LetIn of 'term * 'ident + | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option + | TacticAst.Replace_pattern of 'term pattern * 'term + | TacticAst.Rewrite of direction * 'term * 'ident option + *) + | _ -> + MatitaTypes.not_implemented "some tactic" + in let shared = new sharedState ~disambiguator ~proof_handler ~console () in object (self) inherit interpreterState ~console @@ -164,8 +189,14 @@ class proofState method evalTactical = function | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical | TacticAst.Command TacticAst.Abort -> - proof_handler.MatitaTypes.set_proof None; + proof_handler.MatitaTypes.abort_proof (); `Command + | TacticAst.Command (TacticAst.Undo steps) -> + (proof_handler.MatitaTypes.get_proof ())#undo ?steps (); + `Proof + | TacticAst.Command (TacticAst.Redo steps) -> + (proof_handler.MatitaTypes.get_proof ())#redo ?steps (); + `Proof | TacticAst.Seq tacticals -> (* TODO Zack check for proof completed at each step? *) List.iter (fun t -> ignore (self#evalTactical t)) tacticals; diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 58a6f7a96..97449912d 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -52,7 +52,6 @@ let list_map_fail f = (* End of the list utility functions *) -(* class sequent_viewer obj = object(self) @@ -100,15 +99,19 @@ class sequent_viewer obj = | None -> assert false (* "ERROR: No current term!!!" *) ) selections - method load_sequent metasenv sequent = - let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) = - mml_of_cic_sequent metasenv sequent - in - self#load_root ~root:sequent_mml#get_documentElement ; - current_infos <- - Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) + method load_sequent (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata) + sequent_no + = + let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, + ids_to_hypotheses) + = + try + List.assoc sequent_no (snd metadata) + with Not_found -> assert false + in + current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); + self#load_root ~root:mml#get_documentElement end -*) class proof_viewer obj = object(self) @@ -123,7 +126,7 @@ class proof_viewer obj = method load_proof (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata) = let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = - metadata + (fst metadata) in current_infos <- Some @@ -142,7 +145,6 @@ class proof_viewer obj = (** constructors *) -(* let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> @@ -150,7 +152,6 @@ let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = (new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) [] -*) let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 0aef1cc18..6e43d130b 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -35,7 +35,6 @@ val proof_viewer : unit -> MatitaTypes.proof_viewer -(* val sequent_viewer : ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> @@ -47,5 +46,4 @@ val sequent_viewer : ?show:bool -> unit -> MatitaTypes.sequent_viewer -*) diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml index 17b44ffd3..4f485445d 100644 --- a/helm/matita/matitaProof.ml +++ b/helm/matita/matitaProof.ml @@ -29,16 +29,42 @@ let currentProof (uri, metasenv, bo, ty) = (* TODO CSC: Wrong: [] is just plainly wrong *) Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []) +let init_metadata status = + let ((_, metasenv, _, _) as proof, _) = status in + let proof_object_metadata = (* compute proof annotations *) + Cic2acic.acic_object_of_cic_object (currentProof proof) + in + let sequents_metadata = (* compute all sequent annotations from scratch *) + List.map + (fun ((metano, context, term) as sequent) -> + (metano, Cic2acic.asequent_of_sequent metasenv sequent)) + metasenv + in + (proof_object_metadata, sequents_metadata) + +let compute_metadata (old_status, old_metadata) new_status = + let ((_, new_metasenv, _, _) as new_proof, _) = new_status in + let proof_object_metadata = (* compute proof annotations *) + Cic2acic.acic_object_of_cic_object (currentProof new_proof) + in + let sequents_metadata = (* compute all sequent annotations from scratch *) + (** TODO Zack could we reuse some of the annotations from the previous + * status to avoid recomputing all of them? uhm ... we have to which + * sequents haven't been changed by last tactic applications ... doh! *) + List.map + (fun ((metano, context, term) as sequent) -> + (metano, Cic2acic.asequent_of_sequent new_metasenv sequent)) + new_metasenv + in + (proof_object_metadata, sequents_metadata) + class proof ?uri ~typ ~metasenv ~body () = object (self) inherit [MatitaTypes.hist_metadata] - StatefulProofEngine.status ?uri ~typ ~body ~metasenv - (fun proof -> - Cic2acic.acic_object_of_cic_object (currentProof (fst proof))) - (fun (old_proof, old_metadata) new_proof -> - Cic2acic.acic_object_of_cic_object (currentProof (fst new_proof))) - () + StatefulProofEngine.status + ~history_size:BuildTimeConf.history_size ?uri ~typ ~body ~metasenv + init_metadata compute_metadata () method toXml = let currentproof = currentProof self#proof in diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 70f912ae0..2bc5e726b 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -78,13 +78,23 @@ class type disambiguator = end type hist_metadata = - Cic.annobj * - (Cic.id, Cic.term) Hashtbl.t * - (Cic.id, Cic.id option) Hashtbl.t * - (Cic.id, string) Hashtbl.t * - (Cic.id, Cic2acic.anntypes) Hashtbl.t * - (Cic.id, Cic.conjecture) Hashtbl.t * - (Cic.id, Cic.hypothesis) Hashtbl.t + ( (** proof object part *) + (Cic.annobj * (** annotated object *) + (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *) + (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *) + (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *) + (Cic.id, Cic2acic.anntypes) Hashtbl.t * (** ids_to_inner_types *) + (Cic.id, Cic.conjecture) Hashtbl.t * (** ids_to_conjectures *) + (Cic.id, Cic.hypothesis) Hashtbl.t) (** ids_to_hypotheses *) + * (** sequents part *) + ((int * (** sequent (meta) index *) + (Cic.annconjecture * (** annotated conjecture *) + (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *) + (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *) + (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *) + (Cic.id, Cic.hypothesis) Hashtbl.t)) (** ids_to_hypotheses *) + list) + ) class type proof = object @@ -98,7 +108,7 @@ class type proof = type proof_handler = { get_proof: unit -> proof; (* return current proof or fail *) - set_proof: proof option -> unit; (* set a proof option as current proof *) + abort_proof: unit -> unit;(* abort current proof, cleaning up garbage *) has_proof: unit -> bool; (* check if a current proof is available or not *) new_proof: proof -> unit; (* as a set_proof but takes care also to register observers *) @@ -125,7 +135,6 @@ type mml_of_cic_object = (string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document - (** TODO Zack to be reviewed and unified with proof_viewer above *) class type sequent_viewer = object inherit GMathViewAux.multi_selection_math_view @@ -139,15 +148,13 @@ class type sequent_viewer = method get_selected_hypotheses: Cic.hypothesis list (** load a sequent and render it into parent widget *) - method load_sequent: Cic.metasenv -> Cic.conjecture -> unit + method load_sequent: Gdome.document -> hist_metadata -> int -> unit end class type proof_viewer = object inherit GMathViewAux.single_selection_math_view - (** @return the annotated cic term and the ids_to_inner_types and - * ids_to_inner_sorts maps *) method load_proof: Gdome.document -> hist_metadata -> unit end