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 *)
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 =
let get_id (node: Gdome.element) =
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 goal2win = [] (* associative list: goal no -> scrolled win *)
val mutable _metasenv = []
val mutable scrolledWin: GBin.scrolled_window option = None
- (* scrolled window to which cicMathView is currently attached *)
+ (* scrolled window to which the sequentViewer is currently attached *)
+ val logo = (GMisc.image ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png") () :> GObj.widget)
+
+ val logo_with_qed = (GMisc.image ~file:"logo/matita_small.png" () :> GObj.widget)
+
+ method load_logo =
+ notebook#set_show_tabs false;
+ notebook#append_page logo
+
+ method load_logo_with_qed =
+ notebook#set_show_tabs false;
+ notebook#append_page logo_with_qed
method private tab_label metano =
(GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
w#remove cicMathView#coerce;
scrolledWin <- None
| None -> ());
- for i = 1 to pages do notebook#remove_page 0 done;
+ for i = 0 to pages do notebook#remove_page 0 done;
+ notebook#set_show_tabs true;
pages <- 0;
page2goal <- [];
goal2page <- [];
| `String of string
]
-let reloadable = function
- | `About `Current_proof
- | `Dir _ ->
- true
- | _ -> false
-
class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
()
=
ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
self#load (`About `Current_proof))));
ignore (win#browserRefreshButton#connect#clicked
- (handle_error' self#refresh));
+ (handle_error' (self#refresh ~force:true)));
ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
ignore (win#browserForwardButton#connect#clicked
(handle_error' self#forward));
toplevel#show ()
val mutable current_entry = `About `Blank
- val mutable current_infos = None
val model =
new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
(* loads a uri which can be a cic uri or an about:* uri
* @param uri string *)
- method private _load entry =
+ method private _load ?(force=false) entry =
try
- if entry <> current_entry || reloadable entry then begin
+ if entry <> current_entry || entry = `About `Current_proof || force then
+ begin
(match entry with
| `About `Current_proof -> self#home ()
| `About `Blank -> self#blank ()
method win = win
method history = history
method currentEntry = current_entry
- method refresh () =
- if reloadable current_entry then self#_load current_entry
+ method refresh ~force () = self#_load ~force current_entry
end
(self#get_browser reuse)#load entry
end
-let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
+let refresh_all_browsers () =
+ List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers
let update_font_sizes () =
List.iter (fun b -> b#updateFontSize) !cicBrowsers;