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)
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
| 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.
+ * <m:mi xlink:href="...">bool</m:mi> *)
+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)
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;
false
method private popup_contextual_menu time =
-(* prerr_endline "popup_contextual_menu"; *)
match self#string_of_selection with
| None -> ()
| Some s ->
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
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
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 ->
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
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 ());
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;
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:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png") ()
+ :> GObj.widget)
+
+ val logo_with_qed = (GMisc.image
+ ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_small.png") ()
+ :> GObj.widget)
method load_logo =
notebook#set_show_tabs false;
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
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 () =
toplevel#show ()
val mutable current_entry = `About `Blank
- val mutable current_infos = None
val model =
new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
(** 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 = MatitaMisc.trim_blanks txt in
let fix_uri txt =
UriManager.string_of_uri
(UriManager.strip_xpointer (UriManager.uri_of_string txt))
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
projects / helm.git / blobdiff