From: Stefano Zacchiroli Date: Thu, 20 Jan 2005 10:33:50 +0000 (+0000) Subject: snapshot, notably: X-Git-Tag: V_0_1_0~114 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d0991ea0c7c83c100b2d223644cb2f11a8554fa1;p=helm.git snapshot, notably: - added hyperlink handling in check and proof window - start implementation of cic browser --- diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 3d76d0d85..6a2a88623 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -65,7 +65,7 @@ matitac.opt: $(LIBX_DEPS) $(CMXS) matitac.ml matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade $(LABLGLADECC) $< > matitaGeneratedGui.ml - $(OCAMLC) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli + $(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli %.cmi: %.mli $(OCAMLC) $(PKGS) -c $< diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index aca8b98d6..6aee8a561 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -1,8 +1,8 @@
- mowgli.cs.unibo.it - + + localhost
matita.glade @@ -12,8 +12,8 @@
$(prefs.server) helm - - matita + mowgli +
remote diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 103e27673..12b772a95 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -513,7 +513,7 @@ True False False - GDK_WINDOW_TYPE_HINT_NORMAL + GDK_WINDOW_TYPE_HINT_TOOLBAR GDK_GRAVITY_NORTH_WEST @@ -2261,4 +2261,244 @@ Copyright (C) 2004, + + Cic browser + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + + + + True + True + False + + + + True + False + 0 + + + + True + False + 0 + + + + True + True + True + GTK_RELIEF_NORMAL + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-go-back + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + 0 + False + False + + + + + + True + True + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-go-forward + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + + + + True + True + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-home + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + + + + True + gtk-yes + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + True + + + + + + True + + + 0 + True + True + + + + + 0 + False + True + + + + + + True + True + True + True + GTK_POS_TOP + False + False + + + + + + + + True + current proof + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + + + + 0 + True + True + + + + + + + + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 364b58025..107691932 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -87,11 +87,20 @@ let _ = (* attach observers to proof status *) false); currentProof#connect `Abort (fun () -> sequents_viewer#reset; false) +let mathViewer = MatitaMathView.mathViewer () let interpreter = let console = (gui#console :> MatitaTypes.console) in let currentProof = (currentProof :> MatitaTypes.currentProof) in new MatitaInterpreter.interpreter - ~disambiguator ~currentProof ~console ~dbd () + ~disambiguator ~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) (** {2 Script window handling} *) @@ -214,5 +223,6 @@ let _ = (try load_script Sys.argv.(1) with Invalid_argument _ -> ()); + gui#console#show (); GtkThread.main () diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 2f36fc647..3d40e949e 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -198,8 +198,10 @@ class console self#buffer#insert msg; paned#set_position (self#get_max_position - console_height); self#misc#grab_focus () - method hide () = - paned#set_position self#get_max_position + method hide () = (* ZACK still not sure about the gui, for the moment just + * keep the console persistent *) + () +(* paned#set_position self#get_max_position *) method toggle () = let pos = self#get_position in if pos > self#get_max_position - console_height then diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index f21a1967b..e9db307d4 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -777,9 +777,89 @@ class textDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = toplevel#destroy () method check_widgets () = () end +class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"BrowserWin" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel = + new GWindow.window (GtkWindow.Window.cast + (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata)) + method toplevel = toplevel + val browserWin = + new GWindow.window (GtkWindow.Window.cast + (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata)) + method browserWin = browserWin + val browserWinEventBox = + new GBin.event_box (GtkBin.EventBox.cast + (Glade.get_widget_msg ~name:"BrowserWinEventBox" ~info:"GtkEventBox" xmldata)) + method browserWinEventBox = browserWinEventBox + val vbox7 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"vbox7" ~info:"GtkVBox" xmldata)) + method vbox7 = vbox7 + val hbox7 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"hbox7" ~info:"GtkHBox" xmldata)) + method hbox7 = hbox7 + val browserBackButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"BrowserBackButton" ~info:"GtkButton" xmldata)) + method browserBackButton = browserBackButton + val alignment3 = + new GBin.alignment (GtkBin.Alignment.cast + (Glade.get_widget_msg ~name:"alignment3" ~info:"GtkAlignment" xmldata)) + method alignment3 = alignment3 + val hbox6 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"hbox6" ~info:"GtkHBox" xmldata)) + method hbox6 = hbox6 + val image188 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image188" ~info:"GtkImage" xmldata)) + method image188 = image188 + val label10 = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"label10" ~info:"GtkLabel" xmldata)) + method label10 = label10 + val browserForwardButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"BrowserForwardButton" ~info:"GtkButton" xmldata)) + method browserForwardButton = browserForwardButton + val image189 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image189" ~info:"GtkImage" xmldata)) + method image189 = image189 + val browserHomeButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"BrowserHomeButton" ~info:"GtkButton" xmldata)) + method browserHomeButton = browserHomeButton + val image190 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image190" ~info:"GtkImage" xmldata)) + method image190 = image190 + val image187 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata)) + method image187 = image187 + val browserNotebook = + new GPack.notebook (GtkPack.Notebook.cast + (Glade.get_widget_msg ~name:"BrowserNotebook" ~info:"GtkNotebook" xmldata)) + method browserNotebook = browserNotebook + val label9 = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"label9" ~info:"GtkLabel" xmldata)) + method label9 = label9 + method reparent parent = + browserWinEventBox#misc#reparent parent; + toplevel#destroy () + method check_widgets () = () + end let check_all ?(show=false) () = ignore (GMain.Main.init ()); + let browserWin = new browserWin () in + if show then browserWin#toplevel#show (); + browserWin#check_widgets (); let textDialog = new textDialog () in if show then textDialog#toplevel#show (); textDialog#check_widgets (); diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 6572f1a6d..113538361 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -477,4 +477,50 @@ class textDialog : method vbox5 : GPack.box method xml : Glade.glade_xml Gtk.obj end +class browserWin : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val alignment3 : GBin.alignment + val browserBackButton : GButton.button + val browserForwardButton : GButton.button + val browserHomeButton : GButton.button + val browserNotebook : GPack.notebook + val browserWin : GWindow.window + val browserWinEventBox : GBin.event_box + val hbox6 : GPack.box + val hbox7 : GPack.box + val image187 : GMisc.image + val image188 : GMisc.image + val image189 : GMisc.image + val image190 : GMisc.image + val label10 : GMisc.label + val label9 : GMisc.label + 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 browserNotebook : GPack.notebook + method browserWin : GWindow.window + method browserWinEventBox : GBin.event_box + method check_widgets : unit -> unit + method hbox6 : GPack.box + method hbox7 : GPack.box + method image187 : GMisc.image + method image188 : GMisc.image + method image189 : GMisc.image + method image190 : GMisc.image + method label10 : GMisc.label + method label9 : GMisc.label + method reparent : GObj.widget -> unit + 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/matitaGui.ml b/helm/matita/matitaGui.ml index 955ae13e5..f8f252b52 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -38,9 +38,12 @@ 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 ] + check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox; + browser#browserWinEventBox + ] in let console = MatitaConsole.console ~evbox:main#consoleEventBox @@ -62,7 +65,8 @@ 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 about; c fileSel; c main; c proof; c toolbar; c check; c script; + c browser ]); (* key bindings *) List.iter (* global key bindings *) (fun (key, callback) -> self#addKeyBinding key callback) diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 511a59314..bb43d67e0 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -254,10 +254,6 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) = [] indTypes in let cicIndTypes = List.rev cicIndTypes in -(* - prerr_endline uri; - pp_indtypes cicIndTypes; -*) (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) (* TODO Zack a lot more to be done here: @@ -423,7 +419,9 @@ class proofState | _ -> MatitaTypes.not_implemented "some tactic" in - let shared = new sharedState ~disambiguator ~currentProof ~console ~dbd () in + let shared = + new sharedState ~disambiguator ~currentProof ~console ?mathViewer ~dbd () + in object (self) inherit interpreterState ~console diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index d485ac025..f264ec413 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -44,114 +44,122 @@ let list_map_fail f = in aux -let choose_selection mmlwidget (element : Gdome.element option) = - let rec aux element = - if element#hasAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(Gdome.domString "xref") - then - mmlwidget#set_selection (Some element) - else - try - match element#get_parentNode with - | None -> assert false - | Some p -> aux (new Gdome.element_of_node p) - with GdomeInit.DOMCastException _ -> - debug_print "trying to select above the document root" - in - match element with - | Some x -> aux x - | None -> mmlwidget#set_selection None +class clickable_math_view obj = + let href = Gdome.domString "href" in + let xref = Gdome.domString "xref" in + object (self) + inherit GMathViewAux.multi_selection_math_view obj + + val mutable href_callback: (UriManager.uri -> unit) option = None + method set_href_callback f = href_callback <- f + + initializer + ignore (self#connect#selection_changed self#choose_selection); + ignore (self#connect#click (fun (gdome_elt, _, _, _) -> + match gdome_elt with + | Some elt (* element is an hyperlink, use href_callback on it *) + when elt#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href -> + (match href_callback with + | None -> () + | Some f -> + let uri = + elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href + in + f (UriManager.uri_of_string (uri#to_string))) + | Some elt -> ignore (self#action_toggle elt) + | None -> ())) + method private choose_selection gdome_elt = + let rec aux elt = + if elt#hasAttributeNS ~namespaceURI:Misc.helm_ns ~localName:xref then + self#set_selection (Some elt) + else + try + (match elt#get_parentNode with + | None -> assert false + | Some p -> aux (new Gdome.element_of_node p)) + with GdomeInit.DOMCastException _ -> () +(* debug_print "trying to select above the document root" *) + in + match gdome_elt with + | Some elt -> aux elt + | None -> self#set_selection None + end class proof_viewer obj = - object(self) + object(self) - inherit GMathViewAux.single_selection_math_view obj + inherit clickable_math_view obj - val mutable current_infos = None - val mutable current_mathml = None + val mutable current_infos = None + val mutable current_mathml = None - initializer - ignore (self#connect#click (fun (gdome_elt, _, _, _) -> - match gdome_elt with - | Some gdome_elt -> - prerr_endline (gdome_elt#get_nodeName#to_string); - ignore (self#action_toggle gdome_elt) - | None -> ())); - ignore (self#connect#selection_changed (choose_selection self)) - - method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) = - let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, - ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = - Cic2acic.acic_object_of_cic_object (cicCurrentProof proof) - in - current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_conjectures, - ids_to_hypotheses); - let mathml = - ApplyTransformation.mml_of_cic_object ~explode_all:true - (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types - in - 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 + method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) = + let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, + ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = + Cic2acic.acic_object_of_cic_object (cicCurrentProof proof) + in + current_infos <- Some (ids_to_terms, ids_to_father_ids, + ids_to_conjectures, ids_to_hypotheses); + let mathml = + ApplyTransformation.mml_of_cic_object ~explode_all:true + (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types + in + 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) - - inherit GMathViewAux.multi_selection_math_view obj + object(self) - initializer - ignore (self#connect#selection_changed (choose_selection self)) + inherit clickable_math_view obj - val mutable current_infos = None + val mutable current_infos = None - method get_selected_terms = - let selections = self#get_selections in - list_map_fail - (function node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match current_infos with - Some (ids_to_terms,_,_) -> - let id = xpath in - (try - Hashtbl.find ids_to_terms id - with _ -> raise Skip) - | None -> assert false (* "ERROR: No current term!!!" *) - ) selections - - method get_selected_hypotheses = - let selections = self#get_selections in - list_map_fail - (function node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match current_infos with - Some (_,_,ids_to_hypotheses) -> - let id = xpath in - (try - Hashtbl.find ids_to_hypotheses id - with _ -> raise Skip) - | None -> assert false (* "ERROR: No current term!!!" *) - ) selections + method get_selected_terms = + let selections = self#get_selections in + list_map_fail + (fun node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helm_ns + ~localName:(Gdome.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + match current_infos with + | Some (ids_to_terms,_,_) -> + (try + Hashtbl.find ids_to_terms xpath + with _ -> raise Skip) + | None -> assert false) (* "ERROR: No current term!!!" *) + selections + + method get_selected_hypotheses = + let selections = self#get_selections in + list_map_fail + (fun node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helm_ns + ~localName:(Gdome.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + match current_infos with + | Some (_,_,ids_to_hypotheses) -> + (try + Hashtbl.find ids_to_hypotheses xpath + with _ -> raise Skip) + | None -> assert false) (* "ERROR: No current term!!!" *) + selections method load_sequent metasenv metano = (* @@ -281,13 +289,20 @@ let sequents_viewer ~(notebook:GPack.notebook) = new sequents_viewer ~notebook ~sequent_viewer ~set_goal () -let check_widget = - lazy - (let gui = MatitaGui.instance () in - sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add ()) - 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 set_href_callback f = href_callback := f + method checkTerm sequent metasenv = let (metano, context, expr) = sequent in let widget = Lazy.force check_widget in diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index b7a18e920..04d96befe 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -23,16 +23,27 @@ * http://helm.cs.unibo.it/ *) + (** multi selection gtkMathView which handle mactions and hyperlinks. Mactions + * are handled internally. Hyperlinks are handled by calling an user provided + * callback *) +class type clickable_math_view = + object + inherit GMathViewAux.multi_selection_math_view + + (** set hyperlink callback. None disable hyperlink handling *) + method set_href_callback: (UriManager.uri -> unit) option -> unit + end + class type proof_viewer = object - inherit GMathViewAux.single_selection_math_view + inherit clickable_math_view method load_proof: StatefulProofEngine.proof_status -> unit end class type sequent_viewer = object - inherit GMathViewAux.multi_selection_math_view + inherit clickable_math_view (** @return the list of selected terms. Selections which are not terms are * ignored *) diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 5305ea463..c49bce004 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -136,6 +136,7 @@ class type mathViewer = object method checkTerm: Cic.conjecture -> Cic.metasenv -> unit method unload: unit -> unit + method set_href_callback: (UriManager.uri -> unit) option -> unit end type mml_of_cic_sequent = diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index cc91486d6..b0830c709 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -157,6 +157,7 @@ class type mathViewer = object method checkTerm: Cic.conjecture -> Cic.metasenv -> unit method unload: unit -> unit + method set_href_callback: (UriManager.uri -> unit) option -> unit end type mml_of_cic_sequent =