X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=5fe955b3ea5f8124e428b0a7fd28f1815472ee26;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=e572f0982f80d7b6cb1d5d2ddf9b0697f05999d6;hpb=6187b40af194fb960d91653682a0eb2096f20f3b;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index e572f0982..5fe955b3e 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000-2002, HELM Team. +(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -25,32 +25,33 @@ open Printf -open MatitaCicMisc open MatitaTypes -(* List utility functions *) -exception Skip - let list_map_fail f = - let rec aux = - function - [] -> [] - | he::tl -> - try - let he' = f he in - he'::(aux tl) - with Skip -> - (aux tl) - in + let rec aux = function + | [] -> [] + | he::tl -> + try + let he' = f he in + he'::(aux tl) + with Exit -> + (aux tl) + in aux -class clickable_math_view obj = +(** inherit from this class if you want to access current script *) +class scriptAccessor = +object (self) + method private script = MatitaScript.instance () +end + +class clickableMathView 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 + val mutable href_callback: (string -> unit) option = None method set_href_callback f = href_callback <- f initializer @@ -65,7 +66,7 @@ class clickable_math_view obj = let uri = elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href in - f (UriManager.uri_of_string (uri#to_string))) + f (uri#to_string)) | Some elt -> ignore (self#action_toggle elt) | None -> ())) method private choose_selection gdome_elt = @@ -85,18 +86,18 @@ class clickable_math_view obj = | None -> self#set_selection None end -let clickable_math_view ?hadjustment ?vadjustment ?font_size ?log_verbosity = +let clickableMathView ?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)) + (new clickableMathView (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size:None ~log_verbosity:None)) [] -class sequent_viewer obj = +class sequentViewer obj = object(self) - inherit clickable_math_view obj + inherit clickableMathView obj val mutable current_infos = None @@ -113,9 +114,7 @@ class sequent_viewer obj = else match current_infos with | Some (ids_to_terms,_,_) -> - (try - Hashtbl.find ids_to_terms xpath - with _ -> raise Skip) + (try Hashtbl.find ids_to_terms xpath with _ -> raise Exit) | None -> assert false) (* "ERROR: No current term!!!" *) selections @@ -132,70 +131,78 @@ class sequent_viewer obj = else match current_infos with | Some (_,_,ids_to_hypotheses) -> - (try - Hashtbl.find ids_to_hypotheses xpath - with _ -> raise Skip) + (try Hashtbl.find ids_to_hypotheses xpath with _ -> raise Exit) | None -> assert false) (* "ERROR: No current term!!!" *) selections method load_sequent metasenv metano = -(* - let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, - ids_to_hypotheses) = - Cic2acic.asequent_of_sequent metasenv conjecture - in -*) let sequent = CicUtil.lookup_meta metano metasenv in let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) = ApplyTransformation.mml_of_cic_sequent metasenv sequent in current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); +(* debug_print "load_sequent: dumping MathML to ./prova"; ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); +*) self#load_root ~root:mathml#get_documentElement end - -class sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:sequent_viewer) ~set_goal () +class sequentsViewer ~(notebook:GPack.notebook) + ~(sequentViewer:sequentViewer) () = - let tab_label metano = - (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce - in object (self) + inherit scriptAccessor + val mutable pages = 0 val mutable switch_page_callback = None val mutable page2goal = [] (* associative list: page no -> goal no *) val mutable goal2page = [] (* the other way round *) val mutable goal2win = [] (* associative list: goal no -> scrolled win *) val mutable _metasenv = [] + val mutable scrolledWin: GBin.scrolled_window option = None + (* scrolled window to which the sequentViewer is currently attached *) + + method private tab_label metano = + (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce method reset = + (match scrolledWin with + | Some w -> + (* removing page from the notebook will destroy all contained widget, + * we do not want the sequentViewer to be destroyed as well *) + w#remove sequentViewer#coerce; + scrolledWin <- None + | None -> ()); for i = 1 to pages do notebook#remove_page 0 done; pages <- 0; page2goal <- []; goal2page <- []; goal2win <- []; _metasenv <- []; + self#script#setGoal ~-1; (match switch_page_callback with | Some id -> GtkSignal.disconnect notebook#as_widget id; switch_page_callback <- None | None -> ()) - method load_sequents metasenv = + method load_sequents (status: ProofEngineTypes.status) = + let ((_, metasenv, _, _), goal) = status in let sequents_no = List.length metasenv in _metasenv <- metasenv; pages <- sequents_no; + self#script#setGoal goal; let win metano = let w = GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC ~shadow_type:`IN ~show:true () in let reparent () = - match sequent_viewer#misc#parent with - | None -> w#add sequent_viewer#coerce - | Some _ -> sequent_viewer#misc#reparent w#coerce + scrolledWin <- Some w; + match sequentViewer#misc#parent with + | None -> w#add sequentViewer#coerce + | Some _ -> sequentViewer#misc#reparent w#coerce in goal2win <- (metano, reparent) :: goal2win; w#coerce @@ -206,7 +213,7 @@ class sequents_viewer ~(notebook:GPack.notebook) page2goal <- (!page, metano) :: page2goal; goal2page <- (metano, !page) :: goal2page; incr page; - notebook#append_page ~tab_label:(tab_label metano) (win metano)) + notebook#append_page ~tab_label:(self#tab_label metano) (win metano)) metasenv; switch_page_callback <- Some (notebook#connect#switch_page ~callback:(fun page -> @@ -215,14 +222,14 @@ class sequents_viewer ~(notebook:GPack.notebook) List.assoc page page2goal with Not_found -> assert false in - set_goal goal; + self#script#setGoal goal; self#render_page ~page ~goal)) method private render_page ~page ~goal = - sequent_viewer#load_sequent _metasenv goal; + sequentViewer#load_sequent _metasenv goal; try List.assoc goal goal2win (); - sequent_viewer#set_selection None + sequentViewer#set_selection None with Not_found -> assert false method goto_sequent goal = @@ -232,7 +239,7 @@ class sequents_viewer ~(notebook:GPack.notebook) with Not_found -> assert false in notebook#goto_page page; - self#render_page page goal; + self#render_page page goal end @@ -250,27 +257,67 @@ type 'widget constructor = unit -> 'widget -let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = +let sequentViewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params - (new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p)) + (new sequentViewer (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) [] let blank_uri = BuildTimeConf.blank_uri let current_proof_uri = BuildTimeConf.current_proof_uri +type term_source = + [ `Ast of DisambiguateTypes.term + | `Cic of Cic.term * Cic.metasenv + | `String of string + ] + exception Browser_failure of string let cicBrowsers = ref [] -class cicBrowser ~(history:string MatitaMisc.history) () = +class type cicBrowser = +object + method load: MatitaTypes.mathViewer_entry -> unit + (* method loadList: string list -> MatitaTypes.mathViewer_entry-> unit *) + method loadInput: string -> unit +end + +class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) + () += let term_RE = Pcre.regexp "^term:(.*)" in + let whelp_RE = Pcre.regexp "^\\s*whelp" in + let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in + let trailing_slash_RE = Pcre.regexp "/$" in + let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in let gui = MatitaGui.instance () in let win = gui#newBrowserWin () in + let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in + let combo,_ = GEdit.combo_box_text ~strings:queries () in + let activate_combo_query input q = + let q' = String.lowercase q in + let rec aux i = function + | [] -> failwith ("Whelp query '" ^ q ^ "' not found") + | h::_ when String.lowercase h = q' -> i + | _::tl -> aux (i+1) tl + in + combo#set_active (aux 0 queries); + win#queryInputText#set_text input + in + let set_whelp_query txt = + let query, arg = + try + let q = Pcre.extract ~rex:whelp_query_RE txt in + q.(1), q.(2) + with Invalid_argument _ -> failwith "Malformed Whelp query" + in + activate_combo_query arg query + in let toplevel = win#toplevel in - let mathView = sequent_viewer ~packing:win#scrolledBrowser#add () in + let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in let fail msg = ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ()) ~title:"Cic browser" ~msg ~cancel:false ()); @@ -283,11 +330,38 @@ class cicBrowser ~(history:string MatitaMisc.history) () = in let handle_error' f = fun () -> handle_error f in (* used in callbacks *) object (self) + inherit scriptAccessor + + (* Whelp bar queries *) + initializer + activate_combo_query "" "locate"; + win#comboVbox#add (combo :> GObj.widget); + let start_query () = + let query = String.lowercase (List.nth queries combo#active) in + let input = win#queryInputText#text in + let statement = "whelp " ^ query ^ " " ^ input ^ "." in + (MatitaScript.instance ())#advance ~statement () + in + ignore(win#queryInputText#connect#activate ~callback:start_query); + ignore(combo#connect#changed ~callback:start_query); + win#whelpImage2#set_file "icons/whelp.png"; + win#whelpBarToggleButton#set_active false; + win#whelpBarBox#misc#hide (); + win#mathOrListNotebook#set_show_tabs false; + MatitaGtkMisc.connect_toggle_button win#whelpBarToggleButton + (fun () -> + if win#whelpBarToggleButton#active then + win#whelpBarBox#misc#show () + else + win#whelpBarBox#misc#hide ()); + + win#browserForwardButton#misc#set_sensitive false; + win#browserBackButton#misc#set_sensitive false; ignore (win#browserUri#connect#activate (handle_error' (fun () -> - self#_loadUri win#browserUri#text))); + self#loadInput win#browserUri#text))); ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () -> - self#_loadUri current_proof_uri))); + self#_load (`About `Current_proof)))); ignore (win#browserRefreshButton#connect#clicked (handle_error' self#refresh)); ignore (win#browserBackButton#connect#clicked (handle_error' self#back)); @@ -301,71 +375,146 @@ class cicBrowser ~(history:string MatitaMisc.history) () = then GMain.quit (); false)); + ignore(win#whelpResultTreeview#connect#row_activated + ~callback:(fun _ _ -> + let selection = self#_getWhelpResultTreeviewSelection () in + let txt = + if String.sub selection 0 5 = "cic:/" then + selection + else + win#browserUri#text ^ selection + in + self#loadInput txt)); 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 (); + handle_error (fun () -> self#_load (`Uri uri)))); + self#_load (`About `Blank); + toplevel#show () - val disambiguator = MatitaDisambiguator.instance () - val currentProof = MatitaProof.instance () - - val mutable current_uri = "" + val mutable current_entry = `About `Blank val mutable current_infos = None val mutable current_mathml = None + val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview + + method private _getWhelpResultTreeviewSelection () = + match model#easy_selection () with + | [u] -> u + | _ -> assert false + + (** history RATIONALE + * + * all operations about history are done using _historyFoo + * + * only toplevel function like load loadInput can call + * _historyAdd + *) + + method private _historyAdd item = + history#add item; + win#browserBackButton#misc#set_sensitive true; + win#browserForwardButton#misc#set_sensitive false + + method private _historyPrev () = + let item = history#previous in + if history#is_begin then win#browserBackButton#misc#set_sensitive false; + win#browserForwardButton#misc#set_sensitive true; + item + + method private _historyNext () = + let item = history#next in + if history#is_end then win#browserForwardButton#misc#set_sensitive false; + win#browserBackButton#misc#set_sensitive true; + item + + (** notebook RATIONALE + * + * Use only these functions to switch between the tabs + *) + method private _showList = win#mathOrListNotebook#goto_page 1 + method private _showMath = win#mathOrListNotebook#goto_page 0 + + + method private back () = try - self#_loadUri ~add_to_history:false history#previous + self#_load (self#_historyPrev ()) with MatitaMisc.History_failure -> () method private forward () = try - self#_loadUri ~add_to_history:false history#next + self#_load (self#_historyNext ()) with MatitaMisc.History_failure -> () (* loads a uri which can be a cic uri or an about:* uri * @param uri string *) - method private _loadUri ?(add_to_history = true) uri = + method private _load entry = 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 + if entry <> current_entry || entry = `About `Current_proof then begin + (match entry with + | `About `Current_proof -> self#home () + | `About `Blank -> self#blank () + | `About `Us -> () (* TODO implement easter egg here :-] *) + | `Check term -> self#_loadCheck term + | `Cic (term, metasenv) -> self#_loadTermCic term metasenv + | `Dir dir -> self#_loadDir dir + | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri) + | `Whelp (query, results) -> + set_whelp_query query; + self#_loadList results); + self#setEntry entry + end with - | UriManager.IllFormedUri _ -> fail (sprintf "invalid uri: %s" uri) - | CicEnvironment.Object_not_found _ -> - fail (sprintf "object not found: %s" uri) + | UriManager.IllFormedUri uri -> fail (sprintf "invalid uri: %s" uri) + | CicEnvironment.Object_not_found uri -> + fail (sprintf "object not found: %s" (UriManager.string_of_uri uri)) | Browser_failure msg -> fail msg - method loadUri uri = - handle_error (fun () -> self#_loadUri ~add_to_history:true uri) + method private blank () = + self#_showMath; + mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement - method private blank () = mathView#load_root MatitaMisc.empty_mathml + method private _loadCheck term = + failwith "not implemented _loadCheck"; + self#_showMath method private home () = - if currentProof#onGoing () then - self#loadObj (cicCurrentProof currentProof#proof#proof) - else - raise (Browser_failure "no on going proof") + self#_showMath; + match self#script#status.proof_status with + | Proof (uri, metasenv, bo, ty) -> + let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in + let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in + self#_loadObj obj + | Incomplete_proof ((uri, metasenv, bo, ty), _) -> + let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in + let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in + self#_loadObj obj + | _ -> self#blank () (** loads a cic uri from the environment * @param uri UriManager.uri *) - method private loadUriManagerUri 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 + self#_loadObj obj + + method private _loadDir dir = + let content = Http_getter.ls dir in + let l = List.map (function + | Http_getter_types.Ls_section sec -> sec + | Http_getter_types.Ls_object obj -> obj.Http_getter_types.uri + ) content + in + self#_loadList l - method private setUri uri = - win#browserUri#set_text uri; - current_uri <- uri + method private setEntry entry = + win#browserUri#set_text (string_of_entry entry); + current_entry <- entry - method private loadObj obj = + method private _loadObj obj = + self#_showMath; + (* this must be _before_ loading the document, since + * if the widget is not mapped (hidden by the notebook) + * the document is not rendered *) 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,_,_))) = @@ -373,86 +522,131 @@ class cicBrowser ~(history:string MatitaMisc.history) () = in current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses); - match current_mathml with + (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 - - method private _loadTerm s = - self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s)) + current_mathml <- Some mathml); - method private _loadTermAst ast = - let (_, _, term, _) = - MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast - in - self#_loadTermCic term - - method private _loadTermCic term = - let (context, metasenv) = - MatitaCicMisc.get_context_and_metasenv currentProof - in + method private _loadTermCic term metasenv = + let context = self#script#proofContext 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") - + mathView#load_sequent (sequent :: metasenv) dummyno; + self#_showMath + + method private _loadList l = + model#list_store#clear (); + List.iter model#easy_append l; + self#_showList + + (** { public methods, all must call _load!! } *) + + method load uri = + handle_error (fun () -> self#_load uri); + self#_historyAdd uri + + (** this is what the browser does when you enter a string an hit enter *) + method loadInput txt = + let add_terminating_slash s = + if not(Pcre.pmatch ~rex:trailing_slash_RE s) && + not(Pcre.pmatch ~rex:has_xpointer_RE s) then s^"/" else s + in + let is_uri txt = + try + let u = UriManager.strip_xpointer (UriManager.uri_of_string txt) in + ignore(Http_getter.resolve' u); true + with + | Http_getter_types.Key_not_found _ + | Http_getter_types.Unresolvable_URI _ -> false + | UriManager.IllFormedUri u -> failwith ("Malformed URI '" ^ u ^ "'") + in + let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in + if is_whelp txt then + begin + set_whelp_query txt; + + + (MatitaScript.instance ())#advance ~statement:(txt^".") () + end + else + begin + let entry = + if is_uri txt then + (`Uri txt) + else + (`Dir (add_terminating_slash txt)) + in + self#_load entry; + self#_historyAdd entry + end + + (** {2 methods used by constructor only} *) method win = win method history = history - method currentUri = current_uri + method currentEntry = current_entry method refresh () = - if current_uri = current_proof_uri then - self#_loadUri ~add_to_history:false current_proof_uri - + if current_entry = `About `Current_proof then + self#_load (`About `Current_proof) end -let sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:sequent_viewer) ~set_goal () + +let sequentsViewer ~(notebook:GPack.notebook) + ~(sequentViewer:sequentViewer) () = - new sequents_viewer ~notebook ~sequent_viewer ~set_goal () + new sequentsViewer ~notebook ~sequentViewer () let cicBrowser () = let size = BuildTimeConf.browser_history_size in let rec aux history = - let browser = new cicBrowser ~history () in + let browser = new cicBrowser_impl ~history () in let win = browser#win in ignore (win#browserNewButton#connect#clicked (fun () -> let history = - new MatitaMisc.browser_history ~memento:history#save size "" + new MatitaMisc.browser_history ~memento:history#save size + (`About `Blank) in let newBrowser = aux history in - newBrowser#loadUri browser#currentUri)); + newBrowser#load browser#currentEntry)); (* (* 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) + (browser :> cicBrowser) in - let history = new MatitaMisc.browser_history size blank_uri in + let history = new MatitaMisc.browser_history size (`About `Blank) in aux history let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers -class mathViewer = - object - method checkTerm (src:MatitaTypes.term_source) = - (cicBrowser ())#loadTerm src - end +let default_sequentViewer () = sequentViewer ~show:true () +let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer -let mathViewer () = new mathViewer -let instance = MatitaMisc.singleton mathViewer +let default_sequentsViewer () = + let gui = MatitaGui.instance () in + let sequentViewer = sequentViewer_instance () in + sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer () +let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer +let mathViewer () = + object(self) + method private get_browser reuse = + if reuse then + (match !cicBrowsers with + | [] -> cicBrowser () + | b :: _ -> (b :> cicBrowser)) + else + (cicBrowser ()) + + method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t + + method show_uri_list ?(reuse=false) ~entry l = + (self#get_browser reuse)#load entry + end