X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=4c40f9e14588686c9f9d879ab1721658b432eff3;hb=780561e45e8de50dd0063a0e369458ba67479872;hp=188726d9510879720ff984782cd5d8e26fe558d6;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 188726d95..4c40f9e14 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -36,13 +36,13 @@ let debug_print = if debug then prerr_endline else ignore
   (** raised when one of the script margins (top or bottom) is reached *)
 exception Margin
 exception NoUnfinishedProof
-exception ActionCancelled
+exception ActionCancelled of string
 
 let safe_substring s i j =
   try String.sub s i j with Invalid_argument _ -> assert false
 
 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*"
-let heading_nl_RE' = Pcre.regexp "^(\\s*\n\\s*)((.|\n)*)"
+let heading_nl_RE' = Pcre.regexp "^(\\s*\n\\s*)"
 let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
 let multiline_RE = Pcre.regexp "^\n[^\n]+$"
 let newline_RE = Pcre.regexp "\n"
@@ -84,7 +84,10 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
   let initial_space,parsed_text =
    try
     let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
-     pieces.(1), pieces.(2)
+    let p1 = pieces.(1) in
+    let p1_len = String.length p1 in
+    let rest = String.sub parsed_text p1_len (parsed_text_length - p1_len) in
+     p1, rest
    with
     Not_found -> "", parsed_text in
   let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' =
@@ -158,7 +161,7 @@ let wrap_with_developments guistuff f arg =
         else
           f arg
       in
-      let do_nothing () = raise ActionCancelled in
+      let do_nothing () = raise (ActionCancelled "Inclusion not performed") in
       let handle_with_devel d =
         let name = MatitamakeLib.name_for_development d in
         let title = "Unable to include " ^ what in
@@ -218,27 +221,31 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
-  (* XXX use a real CIC -> string pretty printer *)
-  let pp_macro = TAPp.pp_macro ~term_pp:CicPp.ppterm in
+  let pp_macro = 
+    let f t = ProofEngineReduction.replace 
+      ~equality:(fun _ t -> match t with Cic.Meta _ -> true | _ -> false)
+      ~what:[()] ~with_what:[Cic.Implicit None] ~where:t
+    in
+    let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
+    TAPp.pp_macro 
+      ~term_pp:(fun x -> 
+        ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x))
+  in
   match mac with
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) -> 
      let l =  Whelp.match_term ~dbd term in
-     let query_url =
-       MatitaMisc.strip_suffix ~suffix:"."
-         (HExtlib.trim_blanks unparsed_text)
-     in
-     let entry = `Whelp (query_url, l) in
+     let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], parsed_text_length
   | TA.WInstance (loc, term) ->
      let l = Whelp.instance ~dbd term in
-     let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in
+     let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], parsed_text_length
   | TA.WLocate (loc, s) -> 
      let l = Whelp.locate ~dbd s in
-     let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in
+     let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], parsed_text_length
   | TA.WElim (loc, term) ->
@@ -248,13 +255,13 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
        | _ -> failwith "Not a MutInd"
      in
      let l = Whelp.elim ~dbd uri in
-     let entry = `Whelp (pp_macro (TA.WElim (loc, term)), l) in
+     let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], parsed_text_length
   | TA.WHint (loc, term) ->
      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 (pp_macro (TA.WHint (loc, term)), l) in
+     let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], parsed_text_length
   (* REAL macro *)
@@ -321,7 +328,9 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_statu
    begin
     match ex with
      | TA.Command (_,TA.Set (_,"baseuri",u)) ->
-        if not (GrafiteMisc.is_empty u) then
+        if  Http_getter_storage.is_read_only u then
+          raise (ActionCancelled ("baseuri " ^ u ^ " is readonly"));
+        if not (Http_getter_storage.is_empty u) then
          (match 
             guistuff.ask_confirmation 
               ~title:"Baseuri redefinition" 
@@ -330,9 +339,7 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_statu
                 "Do you want to redefine the corresponding "^
                 "part of the library?")
           with
-           | `YES ->
-               let basedir = Helm_registry.get "matita.basedir" in
-                LibraryClean.clean_baseuris ~basedir [u]
+           | `YES -> LibraryClean.clean_baseuris [u]
            | `NO -> ()
            | `CANCEL -> raise MatitaTypes.Cancel)
      | _ -> ()
@@ -414,7 +421,7 @@ class script  ~(source_view: GSourceView.source_view)
               () =
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
-let initial_statuses =
+let initial_statuses () =
  (* these include_paths are used only to load the initial notation *)
  let include_paths =
   Helm_registry.get_list Helm_registry.string "matita.includes" in
@@ -455,7 +462,7 @@ object (self)
 
   val mutable statements = []    (** executed statements *)
 
-  val mutable history = [ initial_statuses ]
+  val mutable history = [ initial_statuses () ]
     (** list of states before having executed statements. Head element of this
       * list is the current state, last element is the state at the beginning of
       * the script.
@@ -532,6 +539,7 @@ object (self)
       self#notify
     with 
     | Margin -> self#notify
+    | Not_found -> assert false
     | exc -> self#notify; raise exc
 
   method retract () =
@@ -645,7 +653,7 @@ object (self)
 
   method private reset_buffer = 
     statements <- [];
-    history <- [ initial_statuses ];
+    history <- [ initial_statuses () ];
     userGoal <- None;
     self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
@@ -800,6 +808,7 @@ object (self)
     try
       is_there_only_comments self#lexicon_status s
     with 
+    | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true