X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=44ead20baf1672260e88037394fcda180c10affd;hb=bd112857523fc543c78cd29b74417585033ec464;hp=2055bb9cdbe3c2a99c7ef25e4722bafbee87dd6e;hpb=341c09ae53c5b432015dbd95ac099d824609e626;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 2055bb9cd..44ead20ba 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -210,7 +210,7 @@ let cic2grafite context menv t =
       | Cic.Const _ as t -> 
           PT.Ident (pp_t c t, None)
       | Cic.Appl l -> PT.Appl (List.map (aux c) l)
-      | Cic.Implicit _ -> PT.Implicit
+      | Cic.Implicit _ -> PT.Implicit `JustOne
       | Cic.Lambda (Cic.Name n, s, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Decl s)::c) t)
@@ -220,7 +220,7 @@ let cic2grafite context menv t =
       | Cic.LetIn (Cic.Name n, s, ty, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
-      | Cic.Meta _ -> PT.Implicit
+      | Cic.Meta _ -> PT.Implicit `JustOne
       | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
       | Cic.Sort Cic.Set -> PT.Sort `Set
       | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
@@ -365,6 +365,34 @@ let cic2grafite context menv t =
   prerr_endline script;
   stupid_indenter script
 ;;
+let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
+  let parsed_text_length = String.length parsed_text in
+  match mac with
+  | TA.Screenshot (_,name) -> 
+       let status = script#grafite_status in
+       let _,_,menv,subst,_ = status#obj in
+       let name = Filename.dirname (script#filename) ^ "/" ^ name in
+       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 _,_,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 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));
+      [status, parsed_text], "", parsed_text_length
 
 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
@@ -593,6 +621,10 @@ script ex loc
       let grafite_status,macro = lazy_macro context in
        eval_macro include_paths buffer guistuff grafite_status
         user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
+   | GrafiteEngine.NMacro (_loc,macro) ->
+       eval_nmacro include_paths buffer guistuff grafite_status
+        user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
+
 
 and eval_statement include_paths (buffer : GText.buffer) guistuff 
  grafite_status user_goal script statement
@@ -623,6 +655,15 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
       let parsed_text, _, _, parsed_text_length = text_of_loc loc in
        [grafite_status,parsed_text],"",
         parsed_text_length
+  | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
+     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
+  | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) 
+    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
   | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> 
       let parsed_text, _, _, parsed_text_length = text_of_loc loc in
       let remain_len = String.length unparsed_text - parsed_text_length in
@@ -645,18 +686,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
       | (statuses,text)::tl ->
          (statuses,parsed_text ^ text)::tl,"",parsed_text_length + len
       | [] -> [], "", 0)
-  | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
-     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
   
 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
@@ -664,9 +699,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
@@ -735,7 +778,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.
@@ -765,12 +808,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
@@ -807,7 +853,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)
@@ -972,12 +1018,12 @@ object (self)
     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;
+    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;