- mathView#load_sequent (sequent :: metasenv) dummyno
-
- method loadTerm (src:MatitaTypes.term_source) =
- handle_error (fun () ->
- (match src with
- | `Ast ast -> self#_loadTermAst ast
- | `Cic cic -> self#_loadTermCic cic
- | `String s -> self#_loadTerm s);
- self#setUri "check")
-
+ mathView#load_sequent (sequent :: metasenv) dummyno;
+ self#_showMath
+
+ method private _loadList l =
+ model#list_store#clear ();
+ List.iter model#easy_append l;
+ self#_showList
+
+ (** { public methods, all must call _load!! } *)
+
+ method load uri =
+ handle_error (fun () -> self#_load uri);
+ self#_historyAdd uri
+
+ (** this is what the browser does when you enter a string an hit enter *)
+ method loadInput txt =
+ let add_terminating_slash s =
+ if not(Pcre.pmatch ~rex:trailing_slash_RE s) &&
+ not(Pcre.pmatch ~rex:has_xpointer_RE s) then s^"/" else s
+ in
+ let is_uri txt =
+ try
+ let u = UriManager.strip_xpointer (UriManager.uri_of_string txt) in
+ ignore(Http_getter.resolve' u); true
+ with
+ | Http_getter_types.Key_not_found _
+ | Http_getter_types.Unresolvable_URI _ -> false
+ | UriManager.IllFormedUri u -> failwith ("Malformed URI '" ^ u ^ "'")
+ in
+ let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
+ if is_whelp txt then
+ begin
+ let q = Pcre.extract ~rex:whelp_query_RE txt in
+ let query, arg =
+ try
+ q.(1), q.(2)
+ with Invalid_argument _ -> failwith "Malformed Whelp query"
+ in
+ activate_combo_query arg query;
+ (MatitaScript.instance ())#advance ~statement:(txt^".") ()
+ end
+ else
+ begin
+ let entry =
+ if is_uri txt then
+ (`Uri txt)
+ else
+ (`Dir (add_terminating_slash txt))
+ in
+ self#_load entry;
+ self#_historyAdd entry
+ end
+
+