X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=4738a38f673dd55bd6b6496358b655194007a32f;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=21450e5e796e7d74c8f7549e156f079799e80646;hpb=4286d368b6d902a4b54c4cf8590c387f2cdb90ea;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 21450e5e7..4738a38f6 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -371,21 +371,61 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
   | TA.Screenshot (_,name) -> 
        let status = script#grafite_status in
        let _,_,menv,subst,_ = status#obj in
-       let sequent = List.hd menv in
        let name = Filename.dirname (script#filename) ^ "/" ^ name in
-       guistuff.mathviewer#screenshot status sequent menv subst name;
+       let sequents = 
+         let selected = Continuationals.Stack.head_goals status#stack in
+         List.filter (fun x,_ -> List.mem x selected) menv         
+       in
+       guistuff.mathviewer#screenshot status sequents menv subst name;
        [status, parsed_text], "", parsed_text_length
   | TA.NCheck (_,t) ->
       let status = script#grafite_status in
-      let ctx = [] in
+      let _,_,menv,subst,_ = status#obj in
+      let ctx = 
+        try let _,(_,ctx,_) = List.hd menv in ctx
+        with Failure "hd" -> []
+      in
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
-          None status [] [] ctx (parsed_text,parsed_text_length,
+          None status ctx menv subst (parsed_text,parsed_text_length,
             CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in
       guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
-      [], "", parsed_text_length
+      [status, parsed_text], "", parsed_text_length
+  | TA.NIntroGuess _loc ->
+      let names_ref = ref [] in
+      let s = 
+        NTactics.intros_tac ~names_ref [] script#grafite_status 
+      in
+      let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+      let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+      [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length
+  | TA.NAutoInteractive (_loc, (None,a)) -> 
+      let trace_ref = ref [] in
+      let s = 
+        NnAuto.auto_tac 
+          ~params:(None,a) ~trace_ref script#grafite_status 
+      in
+      let depth = 
+        try List.assoc "depth" a
+        with Not_found -> ""
+      in
+      let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in
+      let thms = 
+        match !trace_ref with
+        | [] -> "{}"
+        | thms -> 
+           String.concat ", "  
+             (HExtlib.filter_map (function 
+               | CicNotationPt.NRef r -> Some (NCicPp.r2s true r) 
+               | _ -> None) 
+             thms)
+      in
+      let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+      let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+      [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
+  | TA.NAutoInteractive (_, (Some _,_)) -> assert false
 
 let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
   let module MQ = MetadataQuery in
@@ -393,7 +433,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
-  let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:true in
+  let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:false in
   match mac with
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) -> 
@@ -552,13 +592,13 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status
               in
               let ty,_ = 
                 CicTypeChecker.type_of_aux'
-                  menv [] proof_term CicUniv.empty_ugraph
+                  [] [] proof_term CicUniv.empty_ugraph
               in
-              prerr_endline (CicPp.ppterm proof_term);
+              prerr_endline (CicPp.ppterm proof_term ^ " n lambda= " ^ string_of_int how_many_lambdas);
               (* use declarative output *)
               let obj =
                 (* il proof_term vive in cc, devo metterci i lambda no? *)
-                (Cic.CurrentProof ("xxx",menv,proof_term,ty,[],[]))
+                (Cic.CurrentProof ("xxx",[],proof_term,ty,[],[]))
               in
                ApplyTransformation.txt_of_cic_object
                 ~map_unicode_to_tex:(Helm_registry.get_bool
@@ -653,7 +693,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
       eval_executable include_paths buffer guistuff 
        grafite_status user_goal unparsed_text skipped nonskipped script ex loc
   | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) 
-    (*when Helm_registry.get_bool "matita.literate" *) ->
+    when Helm_registry.get_bool "matita.execcomments" ->
      let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
       eval_executable include_paths buffer guistuff 
        grafite_status user_goal unparsed_text skipped nonskipped script ex loc
@@ -684,7 +724,7 @@ let fresh_script_id =
   let i = ref 0 in
   fun () -> incr i; !i
 
-class script  ~(source_view: GSourceView.source_view)
+class script  ~(source_view: GSourceView2.source_view)
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
               ~ask_confirmation
@@ -692,9 +732,17 @@ class script  ~(source_view: GSourceView.source_view)
               () =
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
-let initial_statuses baseuri =
+let initial_statuses current baseuri =
+ let empty_lstatus = new LexiconEngine.status in
+ (match current with
+     Some current ->
+      LexiconSync.time_travel ~present:current ~past:empty_lstatus;
+      GrafiteSync.time_travel ~present:current ();
+      (* CSC: there is a known bug in invalidation; temporary fix here *)
+      NCicEnvironment.invalidate ()
+   | None -> ());
  let lexicon_status =
-   CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
+   CicNotation2.load_notation ~include_paths:[] empty_lstatus
      BuildTimeConf.core_notation_script 
  in
  let grafite_status = GrafiteSync.init lexicon_status baseuri in
@@ -763,7 +811,7 @@ object (self)
 
   val mutable statements = []    (** executed statements *)
 
-  val mutable history = [ initial_statuses default_buri ]
+  val mutable history = [ initial_statuses None default_buri ]
     (** 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.
@@ -793,12 +841,15 @@ object (self)
    let s = match statement with Some s -> s | None -> self#getFuture in
    if self#bos then LibraryClean.clean_baseuris [self#buri_of_current_file];
    HLog.debug ("evaluating: " ^ first_line s ^ " ...");
+   let time1 = Unix.gettimeofday () in
    let entries, newtext, parsed_len = 
     try
      eval_statement self#include_paths buffer guistuff
       self#grafite_status userGoal self (`Raw s)
     with End_of_file -> raise Margin
    in
+   let time2 = Unix.gettimeofday () in
+   HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s");
    let new_statuses, new_statements =
      let statuses, texts = List.split entries in
      statuses, texts
@@ -835,7 +886,7 @@ object (self)
     match history with s::_ -> s | [] -> assert false
    in
     LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
-    GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
+    GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status ();
     statements <- new_statements;
     history <- new_history;
     self#moveMark (- offset)
@@ -960,7 +1011,6 @@ object (self)
       | Some f -> Some (Librarian.absolutize f)
       | None -> None
     in
-    self#goto_top;
     filename_ <- file; 
     include_paths_ <- 
       (match file with Some file -> read_include_paths file | None -> []);
@@ -990,22 +1040,9 @@ object (self)
         HLog.debug ("backup " ^ f ^ " saved")                    
       end
   
-  method private goto_top =
-    let grafite_status = 
-      let rec last x = function 
-      | [] -> x
-      | hd::tl -> last hd tl
-      in
-      last (self#grafite_status) history
-    in
-    (* FIXME: this is not correct since there is no undo for 
-     * library_objects.set_default... *)
-    GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
-    LexiconSync.time_travel ~present:self#grafite_status ~past:grafite_status
-
   method private reset_buffer = 
     statements <- [];
-    history <- [ initial_statuses self#buri_of_current_file ];
+    history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ];
     userGoal <- None;
     self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
@@ -1036,7 +1073,6 @@ object (self)
     match pos with
     | `Top -> 
         dispose_old_locked_mark (); 
-        self#goto_top; 
         self#reset_buffer;
         self#notify
     | `Bottom ->