From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 8 Jun 2005 16:53:28 +0000 (+0000)
Subject: rewritten cicBrowser handling of uri text entry, still some issued with browser
X-Git-Tag: PRE_INDEX_1~24
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8631b0d6a32380ceb540fdb31ccea35ed8c7af18;p=helm.git

rewritten cicBrowser handling of uri text entry, still some issued with browser
history
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 6ca720830..3c141126d 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -25,7 +25,8 @@ let tactic_of_ast = function
       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Intros (_, Some num, names) ->
       (* TODO Zack implement intros length *)
-      PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
+      PrimitiveTactics.intros_tac ~howmany:num
+        ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Contradiction _ -> Tactics.contradiction
@@ -335,7 +336,6 @@ let eval_command status cmd =
         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") 
       in
       let metasenv = MatitaMisc.get_proof_metasenv status in
-      debug_print ("XXXXXXXXXX" ^ CicPp.ppterm body);
       let (body_type, ugraph) =
         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
       in
diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 6db20400e..1cb23366a 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -39,6 +39,17 @@ let list_map_fail f =
   in
   aux
 
+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)
@@ -290,6 +301,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 =
   let term_RE = Pcre.regexp "^term:(.*)" in
   let whelp_RE = Pcre.regexp "^\\s*whelp" in
+  let uri_RE =
+    Pcre.regexp
+      "^cic:/(\\w+/)*\\w+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
+  in
+  let dir_RE = Pcre.regexp "^cic:((/(\\w+/)*\\w+(/)?)|/|)$" in
   let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in
   let trailing_slash_RE = Pcre.regexp "/$" in
   let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in
@@ -510,10 +526,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       
     method private _loadDir dir = 
       let content = Http_getter.ls dir in
-      let l = List.map (function 
-        | Http_getter_types.Ls_section sec -> "dir", sec
-        | Http_getter_types.Ls_object obj -> "obj", obj.Http_getter_types.uri
-        ) content
+      let l =
+        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
       self#_loadList l
 
@@ -556,48 +574,33 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     
     (** { public methods, all must call _load!! } *)
       
-    method load uri =
-      handle_error (fun () -> self#_load uri);
-      self#_historyAdd uri
+    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 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 _
-        | UriManager.IllFormedUri ("cic:/" | "cic:") -> false
-        | UriManager.IllFormedUri u -> failwith ("Malformed URI '" ^ u ^ "'")
-      in
+    method loadInput txt =
+      let txt = strip_blanks txt in
       let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
-      if is_whelp txt then
-        begin
-          set_whelp_query txt;  
-          
-            
-          (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
-      
-        
+      let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
+      let is_dir txt = Pcre.pmatch ~rex:dir_RE 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.instance ())#advance ~statement:(txt ^ ".") ()
+      end else begin
+        let entry =
+          match txt with
+          | txt when is_uri txt -> `Uri (fix_uri txt)
+          | txt when is_dir txt -> `Dir (add_trailing_slash txt)
+          | _ -> raise (Browser_failure (sprintf "unsupported uri: %s" txt))
+        in
+        self#_load entry;
+        self#_historyAdd entry
+      end
+
       (** {2 methods used by constructor only} *)
 
     method win = win
diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli
index aa9d38ded..b11befe4e 100644
--- a/helm/matita/matitaMathView.mli
+++ b/helm/matita/matitaMathView.mli
@@ -59,7 +59,6 @@ class type sequentsViewer =
 
 exception Browser_failure of string
 
-
 class type cicBrowser =
 object
   method load: MatitaTypes.mathViewer_entry -> unit