From ef9ec8cb57d15426a96fe40d056eb07804753bb9 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 1 Feb 2005 17:59:04 +0000 Subject: [PATCH] snapshot, notably: - removed check window and proof window - implemented cicBrowser which can be used to render current proof, term the user wants to check and any other object from the library using a www-browser-like interface --- helm/matita/.depend | 21 ++- helm/matita/buildTimeConf.ml.in | 3 + helm/matita/matita.glade | 95 ++++++++--- helm/matita/matita.ml | 29 ++-- helm/matita/matitaCicMisc.ml | 34 ++++ helm/matita/matitaCicMisc.mli | 48 ++++++ helm/matita/matitaConsole.ml | 55 +++--- helm/matita/matitaGeneratedGui.ml | 68 +++++--- helm/matita/matitaGeneratedGui.mli | 40 +++-- helm/matita/matitaGtkMisc.ml | 15 +- helm/matita/matitaGtkMisc.mli | 23 ++- helm/matita/matitaGui.ml | 22 +-- helm/matita/matitaGui.mli | 4 +- helm/matita/matitaInterpreter.ml | 48 +----- helm/matita/matitaMathView.ml | 263 +++++++++++++++++++++-------- helm/matita/matitaMathView.mli | 49 ++---- helm/matita/matitaMisc.ml | 81 +++++++++ helm/matita/matitaMisc.mli | 26 +++ helm/matita/matitaTypes.ml | 18 +- helm/matita/matitaTypes.mli | 16 +- 20 files changed, 671 insertions(+), 287 deletions(-) create mode 100644 helm/matita/matitaCicMisc.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index 2de9cd092..66e9b07a5 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,5 +1,5 @@ -matitaCicMisc.cmo: matitaTypes.cmi -matitaCicMisc.cmx: matitaTypes.cmx +matitaCicMisc.cmo: matitaTypes.cmi matitaCicMisc.cmi +matitaCicMisc.cmx: matitaTypes.cmx matitaCicMisc.cmi matitac.cmo: matitaTypes.cmi matitaProof.cmi matitaInterpreter.cmi \ matitaDisambiguator.cmi buildTimeConf.cmo matitac.cmx: matitaTypes.cmx matitaProof.cmx matitaInterpreter.cmx \ @@ -18,12 +18,14 @@ matitaGui.cmo: matitaMisc.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmi \ matitaConsole.cmi buildTimeConf.cmo matitaGui.cmi matitaGui.cmx: matitaMisc.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \ matitaConsole.cmx buildTimeConf.cmx matitaGui.cmi -matitaInterpreter.cmo: matitaTypes.cmi matitaProof.cmi matitaInterpreter.cmi -matitaInterpreter.cmx: matitaTypes.cmx matitaProof.cmx matitaInterpreter.cmi -matitaMathView.cmo: matitaTypes.cmi matitaGui.cmi matitaCicMisc.cmo \ - matitaMathView.cmi -matitaMathView.cmx: matitaTypes.cmx matitaGui.cmx matitaCicMisc.cmx \ - matitaMathView.cmi +matitaInterpreter.cmo: matitaTypes.cmi matitaProof.cmi matitaCicMisc.cmi \ + matitaInterpreter.cmi +matitaInterpreter.cmx: matitaTypes.cmx matitaProof.cmx matitaCicMisc.cmx \ + matitaInterpreter.cmi +matitaMathView.cmo: matitaTypes.cmi matitaMisc.cmi matitaGui.cmi \ + matitaGtkMisc.cmi matitaCicMisc.cmi buildTimeConf.cmo matitaMathView.cmi +matitaMathView.cmx: matitaTypes.cmx matitaMisc.cmx matitaGui.cmx \ + matitaGtkMisc.cmx matitaCicMisc.cmx buildTimeConf.cmx matitaMathView.cmi matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi matitaMathView.cmi \ @@ -32,12 +34,13 @@ matita.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi matitaMathView.cmi \ matita.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx matitaMathView.cmx \ matitaInterpreter.cmx matitaGui.cmx matitaGtkMisc.cmx \ matitaDisambiguator.cmx buildTimeConf.cmx -matitaProof.cmo: matitaTypes.cmi matitaCicMisc.cmo buildTimeConf.cmo \ +matitaProof.cmo: matitaTypes.cmi matitaCicMisc.cmi buildTimeConf.cmo \ matitaProof.cmi matitaProof.cmx: matitaTypes.cmx matitaCicMisc.cmx buildTimeConf.cmx \ matitaProof.cmi matitaTypes.cmo: buildTimeConf.cmo matitaTypes.cmi matitaTypes.cmx: buildTimeConf.cmx matitaTypes.cmi +matitaCicMisc.cmi: matitaTypes.cmi matitaConsole.cmi: matitaTypes.cmi matitaDisambiguator.cmi: matitaTypes.cmi matitaGtkMisc.cmi: matitaTypes.cmi matitaGeneratedGui.cmi diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index e75988386..98c033fdb 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -27,7 +27,10 @@ let debug = @DEBUG@;; let version = "0.0.1";; let undo_history_size = 10;; let console_history_size = 100;; +let browser_history_size = 100;; let gtkrc = "@MATITA_GTKRC@";; let base_uri = "cic:/matita";; let phrase_sep = ".";; +let blank_uri = "about:blank";; +let current_proof_uri = "about:current_proof";; diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 58c713292..d9e922f98 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -51,7 +51,7 @@ True - + True gtk-new 1 @@ -70,7 +70,6 @@ True _Proof or definition ... True - @@ -94,7 +93,7 @@ - + True gtk-open 1 @@ -115,7 +114,7 @@ - + True gtk-save 1 @@ -135,7 +134,7 @@ True - + True gtk-save-as 1 @@ -162,7 +161,7 @@ - + True gtk-quit 1 @@ -206,25 +205,14 @@ - + True - Show Proof Window + New Cic Browser True - False - - - True - Show Check Window - True - False - - - - True @@ -2264,6 +2252,7 @@ Copyright (C) 2004, 400 500 + True Cic browser GTK_WINDOW_TOPLEVEL GTK_WIN_POS_NONE @@ -2283,7 +2272,7 @@ Copyright (C) 2004, False - + True False 0 @@ -2294,6 +2283,33 @@ Copyright (C) 2004, False 0 + + + True + True + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-new + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + True @@ -2396,6 +2412,33 @@ Copyright (C) 2004, + + + True + True + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-refresh + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + True @@ -2426,7 +2469,7 @@ Copyright (C) 2004, True - gtk-yes + gtk-jump-to 4 0.5 0.5 @@ -2441,8 +2484,16 @@ Copyright (C) 2004, - + True + True + True + True + 0 + + True + * + False 0 diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 13ec23a6e..e8c030b61 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -53,7 +53,6 @@ let disambiguator = let currentProof = new MatitaProof.currentProof -let proof_viewer = MatitaMathView.proof_viewer_instance () let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () let sequents_viewer = let set_goal goal = @@ -63,10 +62,7 @@ let sequents_viewer = MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook ~sequent_viewer ~set_goal () let _ = (* attach observers to proof status *) - let proof_observer _ (status, ()) = - let ((uri_opt, _, _, _), _) = status in - proof_viewer#load_proof status; - in + let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) = sequents_viewer#reset; (match goal_opt with @@ -76,7 +72,7 @@ let _ = (* attach observers to proof status *) sequents_viewer#goto_sequent goal) in currentProof#addObserver sequents_observer; - currentProof#addObserver proof_observer; + currentProof#addObserver browser_observer; currentProof#connect `Quit (fun () -> (* quit program, asking for confirmation if needed *) if not (currentProof#onGoing ()) || @@ -87,21 +83,21 @@ let _ = (* attach observers to proof status *) false); currentProof#connect `Abort (fun () -> sequents_viewer#reset; false) -let mathViewer = MatitaMathView.mathViewer () -let cicBrowser = MatitaMathView.cicBrowser () +let currentProof = (currentProof :> MatitaTypes.currentProof) +let mathViewer = + MatitaMathView.mathViewer ~disambiguator + ~currentProof:(currentProof :> MatitaTypes.currentProof) () let interpreter = let console = (gui#console :> MatitaTypes.console) in - let currentProof = (currentProof :> MatitaTypes.currentProof) in new MatitaInterpreter.interpreter - ~disambiguator ~currentProof ~console ~mathViewer ~dbd () + ~disambiguator ~currentProof:(currentProof :> MatitaTypes.currentProof) + ~console ~mathViewer ~dbd () let _ = let href_callback uri = let term = CicAst.Uri (UriManager.string_of_uri uri, None) in ignore (interpreter#evalAst (TacticAst.Command (TacticAst.Check term))) in - proof_viewer#set_href_callback (Some href_callback); - sequent_viewer#set_href_callback (Some href_callback); - mathViewer#set_href_callback (Some href_callback) + sequent_viewer#set_href_callback (Some href_callback) (** {2 Script window handling} *) @@ -162,6 +158,9 @@ let _ = gui#console#echo_error (sprintf "Don't know what to do with file: %s\nUnrecognized file format." f))); + ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ -> + let currentProof = (currentProof :> MatitaTypes.currentProof) in + ignore (MatitaMathView.cicBrowser ~disambiguator ~currentProof ()))); connect_button gui#script#scriptWinForwardButton script_forward; connect_button gui#script#scriptWinBackButton script_back; connect_button gui#script#scriptWinJumpButton script_jump; @@ -169,7 +168,7 @@ let _ = let hole = CicAst.UserInput in let tac ast _ = ignore (interpreter#evalAst (A.Tactic ast)) in let tac_w_term ast _ = - gui#console#clear (); +(* gui#console#clear (); *) gui#console#show ~msg:(TacticAstPp.pp_tactic ast) (); gui#main#mainWin#present () in @@ -215,7 +214,7 @@ let _ = List.iter (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t))) sequent_viewer#get_selected_terms); - addDebugItem "show cic browser" (fun () -> gui#browser#browserWin#show ()); + addDebugItem "refresh all browsers" MatitaMathView.refresh_all_browsers; end (** *) diff --git a/helm/matita/matitaCicMisc.ml b/helm/matita/matitaCicMisc.ml index c77ded6be..e6cda3024 100644 --- a/helm/matita/matitaCicMisc.ml +++ b/helm/matita/matitaCicMisc.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +open Printf + (** create a Cic.CurrentProof from a given proof *) let cicCurrentProof (uri, metasenv, bo, ty) = let uri = MatitaTypes.unopt_uri uri in @@ -35,3 +37,35 @@ let cicConstant (uri, metasenv, bo, ty) = (* TODO CSC: Wrong: [] is just plainly wrong *) Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, [], []) +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) + + (** term AST -> Cic.term. Uses disambiguator and change imperatively the + * metasenv as needed *) +let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~currentProof ast = + if currentProof#onGoing () then begin + let proof = currentProof#proof in + let metasenv = proof#metasenv in + let goal = proof#goal in + let context = canonical_context goal metasenv in + let (_, metasenv, term,ugraph) as retval = + disambiguator#disambiguateTermAst ~context ~metasenv ast + in + proof#set_metasenv metasenv; + retval + end else + disambiguator#disambiguateTermAst ast + +let get_context_and_metasenv ~(currentProof:MatitaTypes.currentProof) = + if currentProof#onGoing () then + let proof = currentProof#proof in + let metasenv = proof#metasenv in + let goal = proof#goal in + (canonical_context goal metasenv, metasenv) + else + ([], []) + diff --git a/helm/matita/matitaCicMisc.mli b/helm/matita/matitaCicMisc.mli new file mode 100644 index 000000000..61111aaf1 --- /dev/null +++ b/helm/matita/matitaCicMisc.mli @@ -0,0 +1,48 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + + (** build a CurrentProof object *) +val cicCurrentProof: + UriManager.uri option * Cic.metasenv * Cic.term * Cic.term -> + Cic.obj + + (** build a Constant object *) +val cicConstant: UriManager.uri option * 'a * Cic.term * Cic.term -> Cic.obj + +val canonical_context: int -> (int * 'a * 'b) list -> 'a + + (** term AST -> Cic.term. Uses disambiguator and change imperatively the + * metasenv as needed *) +val disambiguate : + disambiguator:MatitaTypes.disambiguator -> + currentProof:MatitaTypes.currentProof -> + DisambiguateTypes.term -> + DisambiguateTypes.environment * Cic.metasenv * Cic.term * + CicUniv.universe_graph + +val get_context_and_metasenv: + currentProof:MatitaTypes.currentProof -> + Cic.context * Cic.metasenv + diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 3d40e949e..8dc43a093 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -29,8 +29,7 @@ open MatitaTypes type callback = string -> command_outcome -(* let default_prompt = "# " *) -let default_prompt = "" +let default_prompt = "# " let default_phrase_sep = "." let default_callback = fun (phrase: string) -> (true, true) let bullet = "∙" @@ -41,34 +40,6 @@ 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) ?evbox ~(paned:GPack.paned) obj @@ -92,7 +63,8 @@ class console method ignore_insert_text_signal ignore = _ignore_insert_text_signal <- ignore - val history = new history BuildTimeConf.console_history_size + val history = + new MatitaMisc.shell_history BuildTimeConf.console_history_size val mutable handle_position = 450 val mutable last_phrase = "" @@ -105,6 +77,22 @@ class console * beginning of user input not yet processed *) ignore (buf#create_mark ~name:"USER_INPUT_START" ~left_gravity:true buf#start_iter); + MatitaGtkMisc.connect_key self#event ~modifiers:[`CONTROL] ~stop:true + GdkKeysyms._Return + (fun () -> + buf#insert ~iter:buf#end_iter "\n"; + let inserted_text = + MatitaMisc.strip_trailing_blanks + (buf#get_text + ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START")) + ~stop:buf#end_iter ()) + in + self#invoke_callback inserted_text; + self#echo_prompt ()); + +(* + (* callback handling based on phrase terminator (e.g. ";;" at the end of + * the row: each time a character is inserted *) ignore (buf#connect#after#insert_text (fun iter text -> if (not _ignore_insert_text_signal) && (iter#compare buf#end_iter = 0) && (* insertion at end *) @@ -123,6 +111,7 @@ class console self#invoke_callback inserted_text; self#echo_prompt () end)); +*) (match evbox with (* history key bindings *) | None -> () | Some evbox -> @@ -212,9 +201,9 @@ class console (** navigation methods: history, cursor motion, ... *) method private previous_phrase = - try self#set_phrase history#previous with History_failure -> () + try self#set_phrase history#previous with MatitaMisc.History_failure -> () method private next_phrase = - try self#set_phrase history#next with History_failure -> () + try self#set_phrase history#next with MatitaMisc.History_failure -> () method wrap_exn: 'a. (unit -> 'a) -> 'a option = fun f -> diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index 689984774..b192fd732 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -36,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 image182 = + val image224 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image182" ~info:"GtkImage" xmldata)) - method image182 = image182 + (Glade.get_widget_msg ~name:"image224" ~info:"GtkImage" xmldata)) + method image224 = image224 val newMenu_menu = new GMenu.menu (GtkMenu.Menu.cast (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata)) @@ -56,26 +56,26 @@ 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 image183 = + val image225 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image183" ~info:"GtkImage" xmldata)) - method image183 = image183 + (Glade.get_widget_msg ~name:"image225" ~info:"GtkImage" xmldata)) + method image225 = image225 val saveMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveMenuItem = saveMenuItem - val image184 = + val image226 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image184" ~info:"GtkImage" xmldata)) - method image184 = image184 + (Glade.get_widget_msg ~name:"image226" ~info:"GtkImage" xmldata)) + method image226 = image226 val saveAsMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveAsMenuItem = saveAsMenuItem - val image185 = + val image227 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image185" ~info:"GtkImage" xmldata)) - method image185 = image185 + (Glade.get_widget_msg ~name:"image227" ~info:"GtkImage" xmldata)) + method image227 = image227 val separator1 = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata)) @@ -84,10 +84,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata)) method quitMenuItem = quitMenuItem - val image186 = + val image228 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image186" ~info:"GtkImage" xmldata)) - method image186 = image186 + (Glade.get_widget_msg ~name:"image228" ~info:"GtkImage" xmldata)) + method image228 = image228 val editMenu = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata)) @@ -104,14 +104,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (Glade.get_widget_msg ~name:"ShowToolBarMenuItem" ~info:"GtkCheckMenuItem" xmldata)) method showToolBarMenuItem = showToolBarMenuItem - val showProofMenuItem = - new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast - (Glade.get_widget_msg ~name:"ShowProofMenuItem" ~info:"GtkCheckMenuItem" xmldata)) - method showProofMenuItem = showProofMenuItem - val showCheckMenuItem = - new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast - (Glade.get_widget_msg ~name:"ShowCheckMenuItem" ~info:"GtkCheckMenuItem" xmldata)) - method showCheckMenuItem = showCheckMenuItem + val newCicBrowserMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"NewCicBrowserMenuItem" ~info:"GtkMenuItem" xmldata)) + method newCicBrowserMenuItem = newCicBrowserMenuItem val showScriptMenuItem = new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata)) @@ -793,14 +789,22 @@ class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GBin.event_box (GtkBin.EventBox.cast (Glade.get_widget_msg ~name:"BrowserWinEventBox" ~info:"GtkEventBox" xmldata)) method browserWinEventBox = browserWinEventBox - val vbox7 = + val browserVBox = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox7" ~info:"GtkVBox" xmldata)) - method vbox7 = vbox7 + (Glade.get_widget_msg ~name:"BrowserVBox" ~info:"GtkVBox" xmldata)) + method browserVBox = browserVBox val hbox7 = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"hbox7" ~info:"GtkHBox" xmldata)) method hbox7 = hbox7 + val browserNewButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"BrowserNewButton" ~info:"GtkButton" xmldata)) + method browserNewButton = browserNewButton + val image191 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image191" ~info:"GtkImage" xmldata)) + method image191 = image191 val browserBackButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"BrowserBackButton" ~info:"GtkButton" xmldata)) @@ -829,6 +833,14 @@ class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMisc.image (GtkMisc.Image.cast (Glade.get_widget_msg ~name:"image189" ~info:"GtkImage" xmldata)) method image189 = image189 + val browserRefreshButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"BrowserRefreshButton" ~info:"GtkButton" xmldata)) + method browserRefreshButton = browserRefreshButton + val image229 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image229" ~info:"GtkImage" xmldata)) + method image229 = image229 val browserHomeButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"BrowserHomeButton" ~info:"GtkButton" xmldata)) @@ -841,6 +853,10 @@ class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMisc.image (GtkMisc.Image.cast (Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata)) method image187 = image187 + val browserUri = + new GEdit.entry (GtkEdit.Entry.cast + (Glade.get_widget_msg ~name:"BrowserUri" ~info:"GtkEntry" xmldata)) + method browserUri = browserUri val frame1 = new GBin.frame (GtkBin.Frame.cast (Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata)) diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index a84c1328a..26b487b88 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -16,17 +16,18 @@ class mainWin : val helpMenu_menu : GMenu.menu val hideConsoleButton : GButton.button val image169 : GMisc.image - val image182 : GMisc.image - val image183 : GMisc.image - val image184 : GMisc.image - val image185 : GMisc.image - val image186 : GMisc.image + val image224 : GMisc.image + val image225 : GMisc.image + val image226 : GMisc.image + val image227 : GMisc.image + val image228 : 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 newCicBrowserMenuItem : GMenu.menu_item val newDefsMenuItem : GMenu.menu_item val newMenu : GMenu.image_menu_item val newMenu_menu : GMenu.menu @@ -40,9 +41,7 @@ class mainWin : val separator2 : GMenu.menu_item val separator3 : GMenu.menu_item val sequentsNotebook : GPack.notebook - val showCheckMenuItem : GMenu.check_menu_item val showConsoleMenuItem : GMenu.menu_item - val showProofMenuItem : GMenu.check_menu_item val showScriptMenuItem : GMenu.check_menu_item val showToolBarMenuItem : GMenu.check_menu_item val toplevel : GWindow.window @@ -64,17 +63,18 @@ class mainWin : method helpMenu_menu : GMenu.menu method hideConsoleButton : GButton.button method image169 : GMisc.image - method image182 : GMisc.image - method image183 : GMisc.image - method image184 : GMisc.image - method image185 : GMisc.image - method image186 : GMisc.image + method image224 : GMisc.image + method image225 : GMisc.image + method image226 : GMisc.image + method image227 : GMisc.image + method image228 : 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 newCicBrowserMenuItem : GMenu.menu_item method newDefsMenuItem : GMenu.menu_item method newMenu : GMenu.image_menu_item method newMenu_menu : GMenu.menu @@ -89,9 +89,7 @@ class mainWin : method separator2 : GMenu.menu_item method separator3 : GMenu.menu_item method sequentsNotebook : GPack.notebook - method showCheckMenuItem : GMenu.check_menu_item method showConsoleMenuItem : GMenu.menu_item - method showProofMenuItem : GMenu.check_menu_item method showScriptMenuItem : GMenu.check_menu_item method showToolBarMenuItem : GMenu.check_menu_item method toplevel : GWindow.window @@ -487,6 +485,10 @@ class browserWin : val browserBackButton : GButton.button val browserForwardButton : GButton.button val browserHomeButton : GButton.button + val browserNewButton : GButton.button + val browserRefreshButton : GButton.button + val browserUri : GEdit.entry + val browserVBox : GPack.box val browserWin : GWindow.window val browserWinEventBox : GBin.event_box val frame1 : GBin.frame @@ -496,16 +498,21 @@ class browserWin : val image188 : GMisc.image val image189 : GMisc.image val image190 : GMisc.image + val image191 : GMisc.image + val image229 : GMisc.image val label10 : GMisc.label val scrolledBrowser : GBin.scrolled_window val toplevel : GWindow.window - val vbox7 : GPack.box val xml : Glade.glade_xml Gtk.obj method alignment3 : GBin.alignment method bind : name:string -> callback:(unit -> unit) -> unit method browserBackButton : GButton.button method browserForwardButton : GButton.button method browserHomeButton : GButton.button + method browserNewButton : GButton.button + method browserRefreshButton : GButton.button + method browserUri : GEdit.entry + method browserVBox : GPack.box method browserWin : GWindow.window method browserWinEventBox : GBin.event_box method check_widgets : unit -> unit @@ -516,11 +523,12 @@ class browserWin : method image188 : GMisc.image method image189 : GMisc.image method image190 : GMisc.image + method image191 : GMisc.image + method image229 : GMisc.image method label10 : GMisc.label method reparent : GObj.widget -> unit method scrolledBrowser : GBin.scrolled_window method toplevel : GWindow.window - method vbox7 : GPack.box method xml : Glade.glade_xml Gtk.obj end val check_all : ?show:bool -> unit -> unit diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index aebd2dbc9..a0755371b 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -30,6 +30,18 @@ open MatitaTypes let connect_button (button: GButton.button) callback = ignore (button#connect#clicked callback) +let connect_key (ev:GObj.event_ops) ?(modifiers = []) ?(stop = false) key + callback += + ignore (ev#connect#key_press (fun key' -> + let modifiers' = GdkEvent.Key.state key' in + (match key' with + | key' when GdkEvent.Key.keyval key' = key + && List.for_all (fun m -> List.mem m modifiers') modifiers -> + callback (); + stop + | _ -> false))) + 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 ())); @@ -219,7 +231,7 @@ let interactive_interp_choice ~(gui:#gui) choices = GtkThread.main (); (match !interp_no with Some row -> [row] | _ -> raise Cancel) -let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () = +let ask_confirmation ~(gui:#gui) ?(cancel = true) ?(title = "") ?(msg = "") () = let dialog = gui#newConfirmationDialog () in dialog#confirmationDialog#set_title title; dialog#confirmationDialogLabel#set_label msg; @@ -232,6 +244,7 @@ let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () = ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true)); connect_button dialog#confirmationDialogOkButton (return true); connect_button dialog#confirmationDialogCancelButton (return false); + if not cancel then dialog#confirmationDialogCancelButton#misc#hide (); dialog#confirmationDialog#show (); GtkThread.main (); (match !result with None -> assert false | Some r -> r) diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index 92606176c..46e584596 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -37,6 +37,20 @@ val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit val connect_button: GButton.button -> (unit -> unit) -> unit + (** connect a unit -> unit callback to a particular key press event. Event can + * be specified using its keysym and a list of modifiers which must be in + * effect for the callback to be executed. Further signal processing of other + * key press events remains unchanged; further signal processing of the + * specified key press depends on the stop parameter *) +val connect_key: + GObj.event_ops -> + ?modifiers:Gdk.Tags.modifier list -> + ?stop:bool -> (* stop signal handling when the given key has been pressed? + * Defaults to false *) + Gdk.keysym -> (* (= int) the key, see GdkKeysyms.ml *) + (unit -> unit) -> (* callback *) + unit + (** single string column list *) class stringListModel: GTree.view -> @@ -66,8 +80,13 @@ val interactive_user_uri_choice: gui:#gui -> MatitaTypes.choose_uris_callback (** @raise MatitaTypes.Cancel *) val interactive_interp_choice: gui:#gui -> MatitaTypes.choose_interp_callback - (** @return true if user hit "ok" button, false if user hit "cancel" button *) -val ask_confirmation: gui:#gui -> ?title:string -> ?msg:string -> unit -> bool + (** @return true if user hit "ok" button, false if user hit "cancel" button + * @param cancel if set to true a cancel button is shown to the user, otherwise + * it is not (and indeed the function will return true). Defaults to true *) +val ask_confirmation: + gui:#gui -> + ?cancel:bool -> ?title:string -> ?msg:string -> unit -> + bool (** @param multiline (default: false) if true a TextView widget will be used * for prompting the user otherwise a TextEntry widget will be diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index de5240e44..fef22143a 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -38,12 +38,9 @@ class gui file = let proof = new proofWin ~file () in let check = new checkWin ~file () in let script = new scriptWin ~file () in - let browser = new browserWin ~file () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox; - check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox; - browser#browserWinEventBox - ] + check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox ] in let console = MatitaConsole.console ~evbox:main#consoleEventBox @@ -65,16 +62,17 @@ class gui file = (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) (let c w = (w :> unit>) in - [ c about; c fileSel; c main; c proof; c toolbar; c check; c script; - c browser ]); + [ c about; c fileSel; c main; c proof; c toolbar; c check; c script ]); (* key bindings *) List.iter (* global key bindings *) (fun (key, callback) -> self#addKeyBinding key callback) +(* [ GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin; GdkKeysyms._F4, toggle_win ~check:main#showCheckMenuItem check#checkWin; - GdkKeysyms._F5, +*) + [ GdkKeysyms._F5, toggle_win ~check:main#showScriptMenuItem script#scriptWin; GdkKeysyms._x, (fun () -> console#toggle ()); ]; @@ -105,8 +103,10 @@ class gui file = (* script *) (* menus *) toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem; +(* toggle_visibility proof#proofWin main#showProofMenuItem; toggle_visibility check#checkWin main#showCheckMenuItem; +*) toggle_visibility script#scriptWin main#showScriptMenuItem; List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem; main#saveAsMenuItem ]; @@ -114,16 +114,13 @@ class gui file = ignore (main#showConsoleMenuItem#connect#activate console#toggle); (* main *) connect_button main#hideConsoleButton console#hide; -(* (* console *) console#echo_message (sprintf "\tMatita version %s\n" BuildTimeConf.version); console#echo_prompt (); console#misc#grab_focus (); -*) method about = about - method browser = browser method check = check method console = console method fileSel = fileSel @@ -132,6 +129,11 @@ class gui file = method script = script method toolbar = toolbar + method newBrowserWin () = + let win = new browserWin ~file () in + win#check_widgets (); + win + method newUriDialog () = let dialog = new uriChoiceDialog ~file () in dialog#check_widgets (); diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 419dc77eb..1d3f1220b 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -31,10 +31,9 @@ class gui : method setQuitCallback : (unit -> unit) -> unit method setPhraseCallback : (string -> MatitaTypes.command_outcome) -> unit - (** {2 Access to lower-level GTK widgets} *) + (** {2 Access to singleton instances of lower-level GTK widgets} *) method about : MatitaGeneratedGui.aboutWin - method browser : MatitaGeneratedGui.browserWin method check : MatitaGeneratedGui.checkWin method fileSel : MatitaGeneratedGui.fileSelectionWin method main : MatitaGeneratedGui.mainWin @@ -50,6 +49,7 @@ class gui : * methods below create a new window on each invocation. You should * remember to destroy windows after use *) + method newBrowserWin: unit -> MatitaGeneratedGui.browserWin method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index c9d5a7161..78d30c4cd 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -60,38 +60,6 @@ let split_obj = function | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs) | _ -> assert false -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) - -let get_context_and_metasenv (currentProof:MatitaTypes.currentProof) = - if currentProof#onGoing () then - let proof = currentProof#proof in - let metasenv = proof#metasenv in - let goal = proof#goal in - (canonical_context goal metasenv, metasenv) - else - ([], []) - - (** term AST -> Cic.term. Uses disambiguator and change imperatively the - * metasenv as needed *) -let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~currentProof ast = - if currentProof#onGoing () then begin - let proof = currentProof#proof in - let metasenv = proof#metasenv in - let goal = proof#goal in - let context = canonical_context goal metasenv in - let (_, metasenv, term,ugraph) as retval = - disambiguator#disambiguateTermAst ~context ~metasenv ast - in - proof#set_metasenv metasenv; - retval - end else - disambiguator#disambiguateTermAst ast - class virtual interpreterState = (* static values, shared by all states inheriting this class *) let loc = ref None in @@ -167,9 +135,11 @@ class sharedState Quiet | TacticAst.Command (TacticAst.Check term) -> let (_, _, term,ugraph) = - disambiguate ~disambiguator ~currentProof term + MatitaCicMisc.disambiguate ~disambiguator ~currentProof term in - let (context, metasenv) = get_context_and_metasenv currentProof in + let (context, metasenv) = + MatitaCicMisc.get_context_and_metasenv currentProof + in (* this is the Eval Compute let term = CicReduction.whd context term in *) @@ -179,10 +149,9 @@ class sharedState in (* TASSI: here ugraph1 is unused.... FIXME *) let expr = Cic.Cast (term, ty) in - let sequent = (dummyno, context, expr) in (match mathViewer with - | None -> () - | Some v -> v#checkTerm sequent metasenv); + | Some v -> v#checkTerm (`Cic expr) + | _ -> ()); Quiet | TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) -> let uris = @@ -557,7 +526,9 @@ class proofState () = let disambiguate ast = - let (_, _, term, _) = disambiguate ~disambiguator ~currentProof ast in + let (_, _, term, _) = + MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast + in term in (** tactic AST -> ProofEngineTypes.tactic *) @@ -638,7 +609,6 @@ class proofState if not b then failwith "Wrong proof"; add_constant_to_world ~console ~dbd ~uri ~body:bo ~ty ~ugraph (); currentProof#abort (); - (match mathViewer with None -> () | Some v -> v#unload ()); console#echo_message (sprintf "%s defined" suri); New_state Command | TacticAst.Seq tacticals -> diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 1086d5a66..7bf464a9d 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -85,43 +85,13 @@ class clickable_math_view obj = | None -> self#set_selection None end -let clickable_math_view = +let clickable_math_view ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params (new clickable_math_view (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size:None ~log_verbosity:None)) [] -let clickable_math_view () = clickable_math_view () - -class proof_viewer obj = - object (self) - - inherit clickable_math_view obj - - val mutable current_infos = None - val mutable current_mathml = None - - method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) = - let uri = unopt_uri uri_opt in - let obj = cicCurrentProof proof in - let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures, - ids_to_hypotheses,_,_))) = - ApplyTransformation.mml_of_cic_object uri obj - in - current_infos <- Some (ids_to_terms, ids_to_father_ids, - ids_to_conjectures, ids_to_hypotheses); - debug_print "load_proof: dumping MathML to ./proof"; - ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ()); - match current_mathml with - | None -> - self#load_root ~root:mathml#get_documentElement ; - current_mathml <- Some mathml - | Some current_mathml -> - self#freeze; - XmlDiff.update_dom ~from:current_mathml mathml ; - self#thaw - end class sequent_viewer obj = object(self) @@ -268,6 +238,18 @@ class sequents_viewer ~(notebook:GPack.notebook) (** constructors *) +type 'widget constructor = + ?hadjustment:GData.adjustment -> + ?vadjustment:GData.adjustment -> + ?font_size:int -> + ?log_verbosity:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> + unit -> + 'widget + let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> @@ -276,56 +258,159 @@ let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = ~font_size ~log_verbosity)) [] -class cicBrowser = - object (self) - val widget = - let gui = MatitaGui.instance () in - sequent_viewer ~show:true ~packing:gui#browser#scrolledBrowser#add () +let blank_uri = BuildTimeConf.blank_uri +let current_proof_uri = BuildTimeConf.current_proof_uri +exception Browser_failure of string + +let cicBrowsers = ref [] + +class cicBrowser + ~(disambiguator:MatitaTypes.disambiguator) + ~(currentProof:MatitaTypes.currentProof) + ~(history:string MatitaMisc.history) + () += + let term_RE = Pcre.regexp "^term:(.*)" in + let gui = MatitaGui.instance () in + let win = gui#newBrowserWin () in + let toplevel = win#toplevel in + let mathView = sequent_viewer ~packing:win#scrolledBrowser#add () in + let fail msg = + ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ()) + ~title:"Cic browser" ~msg ~cancel:false ()); + in + let handle_error f = + try + f () + with exn -> + fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn)) + in + object (self) initializer - widget#set_href_callback (Some (fun uri -> self#load_uri uri)) + ignore (win#browserUri#connect#activate (fun () -> + self#_loadUri win#browserUri#text)); + ignore (win#browserHomeButton#connect#clicked (fun () -> + self#_loadUri current_proof_uri)); + ignore (win#browserRefreshButton#connect#clicked self#refresh); + ignore (win#browserBackButton#connect#clicked self#back); + ignore (win#browserForwardButton#connect#clicked self#forward); + ignore (win#toplevel#event#connect#delete (fun _ -> + let my_id = Oo.id self in + cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers; + false)); + mathView#set_href_callback (Some (fun uri -> + handle_error (fun () -> self#_loadUri (UriManager.string_of_uri uri)))); + self#_loadUri ~add_to_history:false blank_uri; + toplevel#show (); + + val mutable current_uri = "" + val mutable current_infos = None + val mutable current_mathml = None - method load_uri uri = () - end + method private back () = + try + self#_loadUri ~add_to_history:false history#previous + with MatitaMisc.History_failure -> () -let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = - GtkBase.Widget.size_params - ~cont:(OgtkMathViewProps.pack_return (fun p -> - OgtkMathViewProps.set_params - (new proof_viewer (GtkMathViewProps.MathView_GMetaDOM.create p)) - ~font_size ~log_verbosity)) - [] + method private forward () = + try + self#_loadUri ~add_to_history:false history#next + with MatitaMisc.History_failure -> () -let proof_viewer_instance = - let instance = lazy ( - let gui = MatitaGui.instance () in - proof_viewer ~show:true ~packing:gui#proof#scrolledProof#add () - ) in - fun () -> Lazy.force instance + (* loads a uri which can be a cic uri or an about:* uri + * @param uri string *) + method private _loadUri ?(add_to_history = true) uri = + try + if current_uri <> uri || uri = current_proof_uri then begin + (match uri with + | uri when uri = blank_uri -> self#blank () + | uri when uri = current_proof_uri -> self#home () + | uri when Pcre.pmatch ~rex:term_RE uri -> + self#loadTerm (`String (Pcre.extract ~rex:term_RE uri).(1)) + | _ -> self#loadUriManagerUri (UriManager.uri_of_string uri)); + self#setUri uri; + if add_to_history then history#add uri + end + with + | UriManager.IllFormedUri _ -> fail (sprintf "invalid uri: %s" uri) + | CicEnvironment.Object_not_found _ -> + fail (sprintf "object not found: %s" uri) + | Browser_failure msg -> fail msg + + method loadUri uri = + handle_error (fun () -> self#_loadUri ~add_to_history:true uri) + + method private blank () = mathView#load_root MatitaMisc.empty_mathml + + method private home () = + if currentProof#onGoing () then + self#loadObj (cicCurrentProof currentProof#proof#proof) + else + raise (Browser_failure "no on going proof") + + (** loads a cic uri from the environment + * @param uri UriManager.uri *) + method private loadUriManagerUri uri = + let uri = UriManager.strip_xpointer uri in + let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + self#loadObj obj + + method private setUri uri = + win#browserUri#set_text uri; + current_uri <- uri + + method private loadObj obj = + let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) + let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures, + ids_to_hypotheses,_,_))) = + ApplyTransformation.mml_of_cic_object obj + in + current_infos <- Some (ids_to_terms, ids_to_father_ids, + ids_to_conjectures, ids_to_hypotheses); + match current_mathml with + | Some current_mathml when use_diff -> + mathView#freeze; + XmlDiff.update_dom ~from:current_mathml mathml; + mathView#thaw + | _ -> + mathView#load_root ~root:mathml#get_documentElement; + current_mathml <- Some mathml -class mathViewer = - let href_callback: (UriManager.uri -> unit) option ref = ref None in - object - val check_widget = - lazy - (let gui = MatitaGui.instance () in - let sequent_viewer = - sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add () - in - sequent_viewer#set_href_callback !href_callback; - sequent_viewer) + method private _loadTerm s = + self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s)) - method set_href_callback f = href_callback := f + method private _loadTermAst ast = + let (_, _, term, _) = + MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast + in + self#_loadTermCic term - method checkTerm sequent metasenv = - let (metano, context, expr) = sequent in - let widget = Lazy.force check_widget in - let gui = MatitaGui.instance () in - gui#check#checkWin#show (); - gui#main#showCheckMenuItem#set_active true; - widget#load_sequent (sequent :: metasenv) metano + method private _loadTermCic term = + let (context, metasenv) = + MatitaCicMisc.get_context_and_metasenv currentProof + in + let dummyno = CicMkImplicit.new_meta metasenv [] in + let sequent = (dummyno, context, term) in + mathView#load_sequent (sequent :: metasenv) dummyno + + method loadTerm (src:MatitaTypes.term_source) = + handle_error (fun () -> + (match src with + | `Ast ast -> self#_loadTermAst ast + | `Cic cic -> self#_loadTermCic cic + | `String s -> self#_loadTerm s); + self#setUri "check") + + (** {2 methods used by constructor only} *) + + method win = win + method history = history + method currentUri = current_uri + method refresh () = + if current_uri = current_proof_uri then + self#_loadUri ~add_to_history:false current_proof_uri - method unload () = (proof_viewer_instance ())#unload end let sequents_viewer ~(notebook:GPack.notebook) @@ -333,7 +418,37 @@ let sequents_viewer ~(notebook:GPack.notebook) = new sequents_viewer ~notebook ~sequent_viewer ~set_goal () -let mathViewer () = new mathViewer +let cicBrowser ~disambiguator ~currentProof () = + let size = BuildTimeConf.browser_history_size in + let rec aux history = + let browser = new cicBrowser ~disambiguator ~currentProof ~history () in + let win = browser#win in + ignore (win#browserNewButton#connect#clicked (fun () -> + let history = + new MatitaMisc.browser_history ~memento:history#save size "" + in + let newBrowser = aux history in + newBrowser#loadUri browser#currentUri)); +(* + (* attempt (failed) to close windows on CTRL-W ... *) + MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL] + GdkKeysyms._W (fun () -> win#toplevel#destroy ()); +*) + cicBrowsers := browser :: !cicBrowsers; + (browser :> MatitaTypes.cicBrowser) + in + let history = new MatitaMisc.browser_history size blank_uri in + aux history + +let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers + +class mathViewer ~disambiguator ~currentProof = + object + method checkTerm (src:MatitaTypes.term_source) = + let browser = cicBrowser ~disambiguator ~currentProof () in + browser#loadTerm src + end -let cicBrowser () = new cicBrowser +let mathViewer ~disambiguator ~currentProof () = + new mathViewer ~disambiguator ~currentProof diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 8b5ca89ac..de8edc855 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -34,13 +34,6 @@ class type clickable_math_view = method set_href_callback: (UriManager.uri -> unit) option -> unit end -class type proof_viewer = - object - inherit clickable_math_view - - method load_proof: StatefulProofEngine.proof_status -> unit - end - class type sequent_viewer = object inherit clickable_math_view @@ -64,14 +57,10 @@ class type sequents_viewer = method goto_sequent: int -> unit (* to be called _after_ load_sequents *) end -class type cicBrowser = - object - method load_uri: UriManager.uri -> unit - end - (** {2 Constructors} *) -val proof_viewer: + (** meta constructor *) +type 'widget constructor = ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> ?font_size:int -> @@ -81,19 +70,11 @@ val proof_viewer: ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> - proof_viewer + 'widget -val sequent_viewer: - ?hadjustment:GData.adjustment -> - ?vadjustment:GData.adjustment -> - ?font_size:int -> - ?log_verbosity:int -> - ?width:int -> - ?height:int -> - ?packing:(GObj.widget -> unit) -> - ?show:bool -> - unit -> - sequent_viewer +val clickable_math_view: clickable_math_view constructor + +val sequent_viewer: sequent_viewer constructor val sequents_viewer: notebook:GPack.notebook -> @@ -102,13 +83,17 @@ val sequents_viewer: unit -> sequents_viewer -val cicBrowser: unit -> cicBrowser - -val mathViewer: unit -> MatitaTypes.mathViewer +val cicBrowser: + disambiguator:MatitaTypes.disambiguator -> + currentProof:MatitaTypes.currentProof -> + unit -> + MatitaTypes.cicBrowser -(** {2 Singletons} *) +val refresh_all_browsers: unit -> unit - (** singleton proof_viewer instance. - * Uses singleton GUI instance *) -val proof_viewer_instance: unit -> proof_viewer +val mathViewer: + disambiguator:MatitaTypes.disambiguator -> + currentProof:MatitaTypes.currentProof -> + unit -> + MatitaTypes.mathViewer diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 1a55795a5..c3b83fd47 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -49,3 +49,84 @@ let strip_trailing_blanks = let rex = Pcre.regexp "\\s*$" in fun s -> Pcre.replace ~rex s +let empty_mathml = + let doc = + Misc.domImpl#createDocument ~namespaceURI:(Some Misc.mathml_ns) + ~qualifiedName:(Gdome.domString "math") ~doctype:None + in + doc#get_documentElement + +exception History_failure + +type 'a memento = 'a array * int * int * int (* data, hd, tl, cur *) + +class type ['a] history = + object + method add : 'a -> unit + method next : 'a + method previous : 'a + method load: 'a memento -> unit + method save: 'a memento + end + +class shell_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 (self) + 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) + method load (data', hd', tl', cur') = + assert (Array.length data = Array.length data'); + hd <- hd'; tl <- tl'; cur <- cur'; + Array.blit data' 0 data 0 (Array.length data') + method save = (Array.copy data, hd, tl, cur) + end + +class ['a] browser_history ?memento size init = + object (self) + initializer match memento with Some m -> self#load m | _ -> () + val data = Array.create size init + val mutable hd = 0 + val mutable tl = 0 + val mutable cur = 0 + method previous = + if cur = tl then raise History_failure; + cur <- cur - 1; + if cur = ~-1 then cur <- size - 1; + data.(cur) + method next = + if cur = hd then raise History_failure; + cur <- cur + 1; + if cur = size then cur <- 0; + data.(cur) + method add (e:'a) = + cur <- cur + 1; + if cur = size then cur <- 0; + if cur = tl then tl <- tl + 1; + if tl = size then tl <- 0; + hd <- cur; + data.(cur) <- e + method load (data', hd', tl', cur') = + assert (Array.length data = Array.length data'); + hd <- hd'; tl <- tl'; cur <- cur'; + Array.blit data' 0 data 0 (Array.length data') + method save = (Array.copy data, hd, tl, cur) + end + diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 7a9ac0fc6..afaa631a0 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -40,3 +40,29 @@ val append_phrase_sep: string -> string val strip_trailing_blanks: string -> string + (** Gdome.element of a MathML document whose rendering should be blank. Used + * by cicBrowser to render "about:blank" document *) +val empty_mathml: Gdome.element + +exception History_failure + +type 'a memento + +class type ['a] history = + object ('b) + method add : 'a -> unit + method next : 'a (** @raise History_failure *) + method previous : 'a (** @raise History_failure *) + method load: 'a memento -> unit + method save: 'a memento + end + + (** shell like history: new items added at the end of the history + * @param size maximum history size *) +class shell_history : int -> [string] history + + (** browser like history: new items added at the current point of the history + * @param size maximum history size + * @param first element in history (this history is never empty) *) +class ['a] browser_history: ?memento:'a memento -> int -> 'a -> ['a] history + diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index c49bce004..5d6b8e99d 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -43,6 +43,8 @@ let explain = function | CicTextualParser2.Parse_error (floc, msg) -> let (x, y) = CicAst.loc_of_floc floc in sprintf "parse error at character %d-%d: %s" x y msg + | CicEnvironment.Object_not_found uri -> + sprintf "object not found: %s" (UriManager.string_of_uri uri) | exn -> sprintf "Uncaught exception: %s" (Printexc.to_string exn) exception No_proof @@ -132,11 +134,21 @@ class type interpreter = method reset : unit end +type term_source = + [ `Ast of DisambiguateTypes.term + | `Cic of Cic.term + | `String of string + ] + class type mathViewer = object - method checkTerm: Cic.conjecture -> Cic.metasenv -> unit - method unload: unit -> unit - method set_href_callback: (UriManager.uri -> unit) option -> unit + method checkTerm: term_source -> unit + end + +class type cicBrowser = + object + method loadUri: string -> unit + method loadTerm: term_source -> unit end type mml_of_cic_sequent = diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index b0830c709..b165740aa 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -153,11 +153,21 @@ class type interpreter = (** {2 MathML widgets} *) +type term_source = + [ `Ast of DisambiguateTypes.term + | `Cic of Cic.term + | `String of string + ] + class type mathViewer = object - method checkTerm: Cic.conjecture -> Cic.metasenv -> unit - method unload: unit -> unit - method set_href_callback: (UriManager.uri -> unit) option -> unit + method checkTerm: term_source -> unit + end + +class type cicBrowser = + object + method loadUri: string -> unit + method loadTerm: term_source -> unit end type mml_of_cic_sequent = -- 2.39.2