X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=6074fdae75e51717d83fb9fc437cf31c3251db18;hb=b2f2e47efe1e01df81cb7659c30eeb76f1f830da;hp=481b8fd6c8c58e8dd528810de2490bb5f09aa368;hpb=650e3b3c9ff0b9cafb76a0edf8139a53446937ba;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 481b8fd6c..6074fdae7 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -28,17 +28,6 @@ open Printf open MatitaTypes open MatitaGtkMisc -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) @@ -75,7 +64,7 @@ let href_ds = Gdome.domString "href" let xref_ds = Gdome.domString "xref" (* ids_to_terms should not be passed here, is just for debugging *) -let find_root_id annobj id ids_to_father_ids ids_to_terms = +let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types = let find_parent id ids = let rec aux id = (* (prerr_endline (sprintf "id %s = %s" id @@ -98,16 +87,35 @@ let find_root_id annobj id ids_to_father_ids ids_to_terms = | Some parent_id -> parent_id in let mk_ids terms = List.map CicUtil.id_of_annterm terms in + let inner_types = + Hashtbl.fold + (fun _ types acc -> + match types.Cic2acic.annexpected with + None -> types.Cic2acic.annsynthesized :: acc + | Some ty -> ty :: types.Cic2acic.annsynthesized :: acc + ) ids_to_inner_types [] in match annobj with | Cic.AConstant (_, _, _, Some bo, ty, _, _) | Cic.AVariable (_, _, Some bo, ty, _, _) | Cic.ACurrentProof (_, _, _, _, bo, ty, _, _) -> - return_father id (mk_ids [ty; bo]) + return_father id (mk_ids (ty :: bo :: inner_types)) | Cic.AConstant (_, _, _, None, ty, _, _) - | Cic.AVariable (_, _, None, ty, _, _) -> return_father id (mk_ids [ty]) + | Cic.AVariable (_, _, None, ty, _, _) -> + return_father id (mk_ids (ty::inner_types)) | Cic.AInductiveDefinition _ -> assert false (* TODO *) + (** @return string content of a dom node having a single text child node, e.g. + * bool *) +let string_of_dom_node node = + match node#get_firstChild with + | None -> "" + | Some node -> + (try + let text = new Gdome.text_of_node node in + text#get_data#to_string + with GdomeInit.DOMCastException _ -> "") + class clickableMathView obj = let text_width = 80 in object (self) @@ -133,18 +141,15 @@ object (self) val mutable selection_changed = false method private selection_get_cb ctxt ~info ~time = -(* prerr_endline "selection_get_cb"; *) (match self#get_selections with | [] -> () | node :: _ -> ctxt#return (self#string_of_node node)) method private selection_clear_cb sel_event = -(* prerr_endline "selection_clear_cb"; *) self#remove_selections; false method private button_press_cb gdk_button = -(* prerr_endline "button_press_cb"; *) let button = GdkEvent.Button.button gdk_button in if button = left_button then begin button_press_x <- GdkEvent.Button.x gdk_button; @@ -155,7 +160,6 @@ object (self) false method private popup_contextual_menu time = -(* prerr_endline "popup_contextual_menu"; *) match self#string_of_selection with | None -> () | Some s -> @@ -202,7 +206,7 @@ object (self) match href_callback with | None -> () | Some f -> - (match MatitaMisc.split href_value with + (match HExtlib.split href_value with | [ uri ] -> f uri | uris -> let menu = GMenu.menu () in @@ -218,18 +222,18 @@ object (self) method private choose_selection_cb gdome_elt = let (gui: MatitaGuiTypes.gui) = get_gui () in let clipboard = GData.clipboard Gdk.Atom.primary in + let set_selection elt = + self#set_selection (Some elt); + self#coerce#misc#add_selection_target + ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary; + ignore (self#coerce#misc#grab_selection Gdk.Atom.primary) + in let rec aux elt = if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds)#to_string <> "" -(* if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds - && (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns - ~localName:xref_ds)#to_string <> "" *) - then begin - self#set_selection (Some elt); - self#coerce#misc#add_selection_target - ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary; - ignore (self#coerce#misc#grab_selection Gdk.Atom.primary) - end else + then + set_selection elt + else try (match elt#get_parentNode with | None -> assert false @@ -237,6 +241,9 @@ object (self) with GdomeInit.DOMCastException _ -> () in (match gdome_elt with + | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns + ~localName:href_ds)#to_string <> "" -> + set_selection elt | Some elt -> aux elt | None -> self#set_selection None); selection_changed <- true @@ -244,7 +251,7 @@ object (self) method update_font_size = self#set_font_size !current_font_size method private get_term_by_id context cic_info id = - let ids_to_terms, ids_to_hypotheses, _, _ = cic_info in + let ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in try `Term (Hashtbl.find ids_to_terms id) with Not_found -> @@ -257,12 +264,19 @@ object (self) method private find_obj_conclusion id = match self#cic_info with | None - | Some (_, _, _, None) -> assert false - | Some (ids_to_terms, _, ids_to_father_ids, Some annobj) -> - let id = find_root_id annobj id ids_to_father_ids ids_to_terms in - (try Hashtbl.find ids_to_terms id with Not_found -> assert false) + | Some (_, _, _, _, None) -> assert false + | Some (ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) -> + let id = + find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types + in + (try Hashtbl.find ids_to_terms id with Not_found -> assert false) method private string_of_node node = + if node#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href_ds + then string_of_dom_node node + else self#string_of_id_node node + + method private string_of_id_node node = let get_id (node: Gdome.element) = let xref_attr = node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds @@ -349,7 +363,7 @@ object (self) ApplyTransformation.mml_of_cic_sequent metasenv sequent in self#set_cic_info - (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, None)); + (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None)); let name = "sequent_viewer.xml" in MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name); ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); @@ -358,12 +372,12 @@ object (self) method load_object obj = let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) let (mathml, - (annobj, (ids_to_terms, ids_to_father_ids, _, ids_to_hypotheses, _, _))) + (annobj, (ids_to_terms, ids_to_father_ids, _, ids_to_hypotheses, _, ids_to_inner_types))) = ApplyTransformation.mml_of_cic_object obj in self#set_cic_info - (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Some annobj)); + (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); (match current_mathml with | Some current_mathml when use_diff -> self#freeze; @@ -389,8 +403,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = val mutable _metasenv = [] val mutable scrolledWin: GBin.scrolled_window option = None (* scrolled window to which the sequentViewer is currently attached *) - val logo = (GMisc.image ~file:"logo/matita_medium.png" () :> GObj.widget) - val logo_with_qed = (GMisc.image ~file:"logo/matita_small.png" () :> GObj.widget) + val logo = (GMisc.image + ~file:(MatitaMisc.image_path "matita_medium.png") () + :> GObj.widget) + + val logo_with_qed = (GMisc.image + ~file:(MatitaMisc.image_path "matita_small.png") () + :> GObj.widget) method load_logo = notebook#set_show_tabs false; @@ -411,19 +430,19 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = w#remove cicMathView#coerce; scrolledWin <- None | None -> ()); - for i = 0 to pages do notebook#remove_page 0 done; + (match switch_page_callback with + | Some id -> + GtkSignal.disconnect notebook#as_widget id; + switch_page_callback <- None + | None -> ()); + for i = 0 to pages do notebook#remove_page 0 done; notebook#set_show_tabs true; pages <- 0; page2goal <- []; goal2page <- []; goal2win <- []; - _metasenv <- []; + _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 (status: ProofEngineTypes.status) = let ((_, metasenv, _, _), goal) = status in @@ -433,7 +452,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#script#setGoal goal; let win metano = let w = - GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC + GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS ~shadow_type:`IN ~show:true () in let reparent () = @@ -571,9 +590,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let handle_error f = try f () - with exn -> fail (MatitaExcPp.to_string exn) + with exn -> + if Helm_registry.get_bool "matita.catch_top_level_exn" then + fail (MatitaExcPp.to_string exn) + else raise exn in let handle_error' f = (fun () -> handle_error (fun () -> f ())) in + let load_easter_egg = lazy ( + win#easterEggImage#set_file (MatitaMisc.image_path "meegg.png")) + in object (self) inherit scriptAccessor @@ -621,7 +646,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) toplevel#show () val mutable current_entry = `About `Blank - val mutable current_infos = None val model = new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview @@ -664,9 +688,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) * * 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 _showList = win#mathOrListNotebook#goto_page 1 + method private back () = try self#_load (self#_historyPrev ()) @@ -680,13 +704,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (* loads a uri which can be a cic uri or an about:* uri * @param uri string *) method private _load ?(force=false) entry = - try + handle_error (fun () -> if entry <> current_entry || entry = `About `Current_proof || force then begin (match entry with | `About `Current_proof -> self#home () | `About `Blank -> self#blank () - | `About `Us -> () (* TODO implement easter egg here :-] *) + | `About `Us -> self#egg () | `Check term -> self#_loadCheck term | `Cic (term, metasenv) -> self#_loadTermCic term metasenv | `Dir dir -> self#_loadDir dir @@ -696,8 +720,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_loadList (List.map (fun r -> "obj", UriManager.string_of_uri r) results)); self#setEntry entry - end - with exn -> fail (MatitaExcPp.to_string exn) + end) method private blank () = self#_showMath; @@ -707,15 +730,19 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) failwith "not implemented _loadCheck"; self#_showMath + method private egg () = + win#mathOrListNotebook#goto_page 2; + Lazy.force load_easter_egg + method private home () = 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 name = UriManager.name_of_uri (HExtlib.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 name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in self#_loadObj obj | _ -> self#blank () @@ -771,7 +798,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (** this is what the browser does when you enter a string an hit enter *) method loadInput txt = - let txt = strip_blanks txt in + let txt = HExtlib.trim_blanks txt in let fix_uri txt = UriManager.string_of_uri (UriManager.strip_xpointer (UriManager.uri_of_string txt)) @@ -783,7 +810,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt) | txt -> (try entry_of_string txt