- commented out no longer needed macros Redo, Undo, Abort

- bugfix: correctly handles "cic:" and "cic:/" pseudo-uris in cicBrowser
- bugfix: fixed String.sub error on directories shorted than 5 chars

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index cf7939fa7c7ce10300751c9db2a17e3e0dc42492..0178982e9b6de2a83a2cdcf6726324821318bbe2 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -146,6 +146,11 @@ let _ =
       (fun _ ->
          let nb = gui#main#hintNotebook in
          nb#goto_page ((nb#current_page + 1) mod 3));
+    addDebugItem "print (on stdout) \"statement\" grammar entry"
+      (fun _ ->
+        Grammar.print_entry Format.std_formatter
+          (Grammar.Entry.obj CicTextualParser2.statement);
+        Format.pp_print_flush Format.std_formatter ());
   end
 
   (** </DEBUGGING> *)

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 5fe955b3ea5f8124e428b0a7fd28f1815472ee26..0a2e8f90df37fbb5b2423e782333086cf209ec68 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -378,8 +378,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       ignore(win#whelpResultTreeview#connect#row_activated 
         ~callback:(fun _ _ ->
           let selection = self#_getWhelpResultTreeviewSelection () in
+          let is_cic s =
+            try
+              String.sub s 0 5 = "cic:/"
+            with Invalid_argument _ -> false
+          in
           let txt = 
-            if String.sub selection 0 5 = "cic:/" then
+            if is_cic selection then
               selection
             else
               win#browserUri#text ^ selection 
@@ -558,10 +563,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let is_uri txt = 
         try 
           let u = UriManager.strip_xpointer (UriManager.uri_of_string txt) in
-          ignore(Http_getter.resolve' u); true
+          ignore (Http_getter.resolve' u);
+          true
         with
         | Http_getter_types.Key_not_found _ 
-        | Http_getter_types.Unresolvable_URI _ -> false
+        | Http_getter_types.Unresolvable_URI _
+        | UriManager.IllFormedUri ("cic:/" | "cic:") -> false
         | UriManager.IllFormedUri u -> failwith ("Malformed URI '" ^ u ^ "'")
       in
       let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 0d59d6f47fcfc9ba8b8e4031658bf382fcfe76dd..c8fbba9bee8a66c777ff205cb0d351aef5841ff4 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -100,7 +100,7 @@ let eval_with_engine status user_goal parsed_text st =
     else
       new_text
   in
-    [ new_status, new_text ], parsed_text_length, None
+    [ new_status, new_text ], parsed_text_length
 
 let disambiguate term status =
   let module MD = MatitaDisambiguator in
@@ -114,7 +114,8 @@ let disambiguate term status =
   | _ -> assert false
  
 let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text
-script mac =
+  script mac
+=
   let module TA = TacticAst in
   let module TAPp = TacticAstPp in
   let module MQ = MetadataQuery in
@@ -132,18 +133,18 @@ script mac =
       let l =  MQ.match_term ~dbd term in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WMatch (loc, term)), l) in
       mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length, None
+      [], parsed_text_length
   | TA.WInstance (loc, term) ->
       let term = disambiguate term status in
       let l = MQ.instance ~dbd term in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
       mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length, None
+      [], parsed_text_length
   | TA.WLocate (loc, s) -> 
       let l = MQ.locate ~dbd s in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
       mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length, None  
+      [], parsed_text_length
   | TA.WElim (loc, term) ->
       let term = disambiguate term status in
       let uri =
@@ -154,21 +155,21 @@ script mac =
       let l = MQ.elim ~dbd uri in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
       mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length, None  
+      [], parsed_text_length
   | TA.WHint (loc, term) ->
       let term = disambiguate term status in
       let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
       let l = List.map fst (MQ.experimental_hint ~dbd s) in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
       mathviewer#show_uri_list ~reuse:true ~entry l;
-      [], parsed_text_length, None  
+      [], parsed_text_length
   (* REAL macro *)
   | TA.Hint loc -> 
       let s = MatitaMisc.get_proof_status status in
       let l = List.map fst (MQ.experimental_hint ~dbd s) in
       let selected = urichooser l in
       (match selected with
-      | [] -> [], parsed_text_length, None
+      | [] -> [], parsed_text_length
       | [uri] -> 
         let ast = 
           (TA.Executable (loc,
@@ -181,7 +182,7 @@ script mac =
           comment parsed_text ^ 
           "\n" ^ TAPp.pp_statement ast
         in
-        [ new_status , extra_text ], parsed_text_length, None
+        [ new_status , extra_text ], parsed_text_length
       | _ -> assert false)
   | TA.Check (_,term) ->
       let metasenv = MatitaMisc.get_proof_metasenv status in
@@ -199,8 +200,8 @@ script mac =
       let ty,_ = CTC.type_of_aux' metasenv context term ugraph in
       let t_and_ty = Cic.Cast (term,ty) in
       mathviewer#show_entry (`Cic (t_and_ty,metasenv));
-      [], parsed_text_length, None
-  | TA.Abort _ -> 
+      [], parsed_text_length
+(*   | TA.Abort _ -> 
       let rec go_back () =
         let status = script#status.proof_status in
         match status with
@@ -215,7 +216,7 @@ script mac =
   | TA.Undo (_, Some i) ->  [], parsed_text_length, 
       Some (fun () -> for j = 1 to i do script#retract () done)
   | TA.Undo (_, None) -> [], parsed_text_length, 
-      Some (fun () -> script#retract ())
+      Some (fun () -> script#retract ()) *)
   (* TODO *)
   | TA.Quit _ -> failwith "not implemented"
   | TA.Print (_,kind) -> failwith "not implemented"
@@ -249,13 +250,13 @@ user_goal script s =
       let parsed_text, parsed_text_length = text_of_loc loc in
       let remain_len = String.length s - parsed_text_length in
       let s = String.sub s parsed_text_length remain_len in
-      let s,len, act = 
+      let s,len = 
         eval_statement status mathviewer urichooser user_goal script s 
       in
       (match s with
       | (status, text) :: tl ->
-        ((status, parsed_text ^ text)::tl), (parsed_text_length + len), act
-      | [] -> [], 0, None)
+        ((status, parsed_text ^ text)::tl), (parsed_text_length + len)
+      | [] -> [], 0)
   | TacticAst.Executable (loc, ex) ->
       let parsed_text, parsed_text_length = text_of_loc loc in
       eval_executable 
@@ -290,7 +291,7 @@ object (self)
   method private _advance ?statement () =
     let s = match statement with Some s -> s | None -> self#getFuture in
     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
-    let (entries, parsed_len, post_advance_action) = 
+    let (entries, parsed_len) = 
       eval_statement self#status mathviewer urichooser userGoal self s in
     let (new_statuses, new_statements) = List.split entries in
 (*
@@ -306,10 +307,7 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     end;
     let new_text = String.concat "" new_statements in
     buffer#insert ~iter:start new_text;
-    self#moveMark (String.length new_text);
-    match post_advance_action with 
-      | Some f -> f () 
-      | _ -> ()
+    self#moveMark (String.length new_text)
 
   method private _retract () =
     match statements, history with