+ method private forward () =
+ try
+ 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 _load ?(force=false) entry =
+ 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 -> self#egg ()
+ | `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)
+
+ method private blank () =
+ self#_showMath;
+ mathView#load_root (Lazy.force empty_mathml)#get_documentElement
+
+ method private _loadCheck term =
+ 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 (HExtlib.unopt uri) in
+ let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+ self#_loadObj obj
+ | Incomplete_proof { proof = (uri, metasenv, bo, ty) } ->
+ let name = UriManager.name_of_uri (HExtlib.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 =
+ 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 content = Http_getter.ls dir in
+ let l =
+ List.fast_sort
+ Pervasives.compare
+ (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
+ lastDir <- dir;
+ self#_loadList l
+
+ method private setEntry entry =
+ win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry);
+ current_entry <- entry
+
+ method private _loadObj obj =
+ (* showMath must be done _before_ loading the document, since if the
+ * widget is not mapped (hidden by the notebook) the document is not
+ * rendered *)
+ self#_showMath;
+ mathView#load_object obj
+
+ 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;
+ 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 = HExtlib.trim_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.current ())#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 (MatitaMisc.normalize_dir txt)
+ | txt ->
+ (try
+ MatitaTypes.entry_of_string txt
+ with Invalid_argument _ ->
+ raise
+ (GrafiteTypes.Command_error(sprintf "unsupported uri: %s" txt)))
+ in
+ self#_load entry;
+ self#_historyAdd entry
+ end
+
+ (** {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 currentEntry = current_entry
+ method refresh ~force () = self#_load ~force current_entry
+
+ end
+
+let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) ():
+ MatitaGuiTypes.sequentsViewer