X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=4d0eace3ae6f7d6cf6ae1ff8b66e67b3cd05ee82;hb=94c9255e1f3095440f4d49ea1d75443a5a343185;hp=addf9763cc2350125be11b57792f8d41d1a5f506;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index addf9763c..4d0eace3a 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -39,12 +39,33 @@ let list_map_fail f = in aux +let add_trailing_slash = + let rex = Pcre.regexp "/$" in + fun s -> + if Pcre.pmatch ~rex s then s + else s ^ "/" + +let strip_blanks = + let rex = Pcre.regexp "^\\s*([^\\s]*)\\s*$" in + fun s -> + (Pcre.extract ~rex s).(1) + (** inherit from this class if you want to access current script *) class scriptAccessor = object (self) method private script = MatitaScript.instance () end +let cicBrowsers = ref [] + +let default_font_size () = + Helm_registry.get_opt_default Helm_registry.int + ~default:BuildTimeConf.default_font_size "matita.font_size" +let current_font_size = ref ~-1 +let increase_font_size () = incr current_font_size +let decrease_font_size () = decr current_font_size +let reset_font_size () = current_font_size := default_font_size () + class clickableMathView obj = let href = Gdome.domString "href" in let xref = Gdome.domString "xref" in @@ -55,23 +76,24 @@ class clickableMathView obj = method set_href_callback f = href_callback <- f initializer + self#set_font_size !current_font_size; 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 -> + when elt#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href -> (match href_callback with | None -> () | Some f -> let uri = - elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href + elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href in f (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 + if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref then self#set_selection (Some elt) else try @@ -84,6 +106,10 @@ class clickableMathView obj = match gdome_elt with | Some elt -> aux elt | None -> self#set_selection None + + method update_font_size = + self#set_font_size !current_font_size + end let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = @@ -100,14 +126,14 @@ class sequentViewer obj = inherit clickableMathView obj val mutable current_infos = None - + 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 + ~namespaceURI:DomMisc.helm_ns ~localName:(Gdome.domString "xref"))#to_string in if xpath = "" then assert false (* "ERROR: No xref found!!!" *) @@ -124,7 +150,7 @@ class sequentViewer obj = (fun node -> let xpath = ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helm_ns + ~namespaceURI:DomMisc.helm_ns ~localName:(Gdome.domString "xref"))#to_string in if xpath = "" then assert false (* "ERROR: No xref found!!!" *) @@ -143,7 +169,7 @@ class sequentViewer obj = 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 ()); + ignore (DomMisc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); *) self#load_root ~root:mathml#get_documentElement end @@ -276,24 +302,60 @@ type term_source = exception Browser_failure of string -let cicBrowsers = ref [] - class type cicBrowser = object - method loadUri: string -> unit - method loadTerm: term_source -> unit + method load: MatitaTypes.mathViewer_entry -> unit + (* method loadList: string list -> MatitaTypes.mathViewer_entry-> unit *) + method loadInput: string -> unit end -class cicBrowser_impl ~(history:string MatitaMisc.history) () = +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 uri_RE = + Pcre.regexp + "^cic:/(\\w+/)*\\w+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$" + in + let dir_RE = Pcre.regexp "^cic:((/(\\w+/)*\\w+(/)?)|/|)$" 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 is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in + let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in + let is_dir txt = Pcre.pmatch ~rex:dir_RE txt 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 = sequentViewer ~packing:win#scrolledBrowser#add () in - let fail msg = - ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ()) - ~title:"Cic browser" ~msg ~cancel:false ()); + let fail message = + MatitaGtkMisc.report_error ~title:"Cic browser" ~message () + in + let tags = + [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png"); + "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ] in let handle_error f = try @@ -301,15 +363,32 @@ class cicBrowser_impl ~(history:string MatitaMisc.history) () = with exn -> fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn)) in - let handle_error' f = fun () -> handle_error f in (* used in callbacks *) + let handle_error' f = (fun () -> handle_error (fun () -> f ())) in object (self) inherit scriptAccessor + + (* Whelp bar queries *) initializer - ignore (win#browserUri#connect#activate (handle_error' (fun () -> - self#_loadUri win#browserUri#text))); + activate_combo_query "" "locate"; + win#whelpBarComboVbox#add combo#coerce; + 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#whelpBarImage#set_file (MatitaMisc.image_path "whelp.png"); + win#mathOrListNotebook#set_show_tabs false; + + win#browserForwardButton#misc#set_sensitive false; + win#browserBackButton#misc#set_sensitive false; + ignore (win#browserUri#entry#connect#activate (handle_error' (fun () -> + self#loadInput win#browserUri#entry#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)); @@ -323,104 +402,139 @@ class cicBrowser_impl ~(history:string MatitaMisc.history) () = then GMain.quit (); false)); + ignore(win#whelpResultTreeview#connect#row_activated + ~callback:(fun _ _ -> self#loadInput (self#_getSelectedUri ()))); mathView#set_href_callback (Some (fun uri -> - handle_error (fun () -> self#_loadUri uri))); - self#_loadUri ~add_to_history:false blank_uri; - toplevel#show (); + handle_error (fun () -> self#load (`Uri (UriManager.uri_of_string uri))))); + self#_load (`About `Blank); + toplevel#show () - val mutable current_uri = "" + val mutable current_entry = `About `Blank val mutable current_infos = None val mutable current_mathml = None + val model = + new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview + + method private _getSelectedUri () = + match model#easy_selection () with + | [sel] when is_uri sel -> sel (* absolute URI selected *) + | [sel] -> win#browserUri#entry#text ^ sel (* relative URI selected *) + | _ -> assert false + + (** history RATIONALE + * + * All operations about history are done using _historyFoo. + * Only toplevel functions (ATM load and loadInput) 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)) - | uri when Pcre.pmatch ~rex:trailing_slash_RE uri -> self#loadDir uri - | _ -> 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 uri + | `Whelp (query, results) -> + set_whelp_query query; + self#_loadList (List.map (fun r -> "obj", UriManager.string_of_uri r) 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 _loadCheck term = + failwith "not implemented _loadCheck"; + self#_showMath + method private home () = - if self#script#onGoingProof () then - let ((uri, metasenv, bo, ty), _) = self#script#proofStatus in - let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in - let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in - self#loadObj obj - else - self#blank () + 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 - - method private loadDir dir = - let mathml = MatitaMisc.empty_boxml () in + self#_loadObj obj + + method private _loadDir dir = let content = Http_getter.ls dir in - let root = mathml#get_documentElement in - let new_box_elt name = - mathml#createElementNS ~namespaceURI:(Some Misc.boxml_ns) - ~qualifiedName:(Gdome.domString ("b:" ^ name)) + let l = + List.map + (function + | Http_getter_types.Ls_section s -> "dir", s + | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri) + content in - let new_text content = mathml#createTextNode (Gdome.domString content) in - let b_v = new_box_elt "v" in - List.iter - (fun item -> - let b_text = new_box_elt "text" in - let uri, elt = - match item with - | Http_getter_types.Ls_section subdir -> - (dir ^ subdir ^ "/"), (new_text (subdir ^ "/")) - | Http_getter_types.Ls_object obj -> - (dir ^ obj.Http_getter_types.uri), - (new_text obj.Http_getter_types.uri) - in - b_text#setAttributeNS ~namespaceURI:(Some Misc.xlink_ns) - ~qualifiedName:(Gdome.domString "xlink:href") - ~value:(Gdome.domString uri); - ignore (b_v#appendChild ~newChild:(b_text :> Gdome.node)); - ignore (b_text#appendChild ~newChild:(elt :> Gdome.node))) - content; - ignore (root#appendChild ~newChild:(b_v :> Gdome.node)); -(* Misc.domImpl#saveDocumentToFile ~doc:mathml ~name:"pippo" (); *) - mathView#load_root ~root:root - - method private setUri uri = - win#browserUri#set_text uri; - current_uri <- uri - - method private loadObj obj = + if l = [] then raise (Browser_failure "no such directory"); + self#_loadList l + + method private setEntry entry = + win#browserUri#entry#set_text (string_of_entry entry); + current_entry <- entry + + 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,_,_))) = @@ -428,51 +542,72 @@ class cicBrowser_impl ~(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 = failwith "not implemented _loadTerm" -(* TODO self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s)) *) - - method private _loadTermAst ast = failwith "not implemented _loadTermAst" -(* TODO - let (_, metasenv, term, _) = - MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast - in - self#_loadTermCic term metasenv -*) + current_mathml <- Some mathml); 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 + mathView#load_sequent (sequent :: metasenv) dummyno; + self#_showMath + + method private _loadList l = + model#list_store#clear (); + List.iter (fun (tag, s) -> model#easy_append ~tag s) l; + self#_showList + + (** { public methods, all must call _load!! } *) + + method load entry = + handle_error (fun () -> self#_load entry; self#_historyAdd entry) + + (** this is what the browser does when you enter a string an hit enter *) + method loadInput txt = + let txt = strip_blanks txt in + let fix_uri txt = + UriManager.string_of_uri + (UriManager.strip_xpointer (UriManager.uri_of_string txt)) + in + if is_whelp txt then begin + set_whelp_query txt; + (MatitaScript.instance ())#advance ~statement:(txt ^ ".") () + end else begin + let entry = + match txt with + | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt)) + | txt when is_dir txt -> `Dir (add_trailing_slash txt) + | txt -> + (try + entry_of_string txt + with Invalid_argument _ -> + raise (Browser_failure (sprintf "unsupported uri: %s" txt))) + in + self#_load entry; + self#_historyAdd entry + end - method loadTerm (src:term_source) = - handle_error (fun () -> - (match src with - | `Ast ast -> self#_loadTermAst ast - | `Cic (cic, metasenv) -> self#_loadTermCic cic metasenv - | `String s -> self#_loadTerm s); - self#setUri "check") + (** {2 methods accessing underlying GtkMathView} *) + + method updateFontSize = mathView#set_font_size !current_font_size (** {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 sequentsViewer ~(notebook:GPack.notebook) ~(sequentViewer:sequentViewer) () = @@ -485,10 +620,11 @@ let cicBrowser () = 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] @@ -497,11 +633,9 @@ let cicBrowser () = cicBrowsers := browser :: !cicBrowsers; (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 - let default_sequentViewer () = sequentViewer ~show:true () let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer @@ -511,3 +645,25 @@ let default_sequentsViewer () = 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 + +let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers + +let update_font_sizes () = + List.iter (fun b -> b#updateFontSize) !cicBrowsers; + (sequentViewer_instance ())#update_font_size +