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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 8de5ccebc..21450e5e7 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -74,8 +74,6 @@ type guistuff = {
 let eval_with_engine include_paths guistuff grafite_status user_goal
  skipped_txt nonskipped_txt st
 =
-  let module TAPp = GrafiteAstPp in
-  let module DTE = DisambiguateTypes.Environment in
   let parsed_text_length =
     String.length skipped_txt + String.length nonskipped_txt 
   in
@@ -212,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)
@@ -222,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)
@@ -367,13 +365,31 @@ 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 sequent = List.hd menv in
+       let name = Filename.dirname (script#filename) ^ "/" ^ name in
+       guistuff.mathviewer#screenshot status sequent menv subst name;
+       [status, parsed_text], "", parsed_text_length
+  | TA.NCheck (_,t) ->
+      let status = script#grafite_status in
+      let ctx = [] in
+      let m, s, status, t = 
+        GrafiteDisambiguate.disambiguate_nterm 
+          None status [] [] ctx (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
 
 let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
-  let module TAPp = GrafiteAstPp in
   let module MQ = MetadataQuery in
-  let module MDB = LibraryDb in
   let module CTC = CicTypeChecker in
-  let module CU = CicUniv in
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
@@ -485,7 +501,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status
       in
       let t_and_ty = Cic.Cast (term,ty) in
       guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
-      [({grafite_status with proof_status = No_proof}), parsed_text ],"", 
+      [(grafite_status#set_proof_status No_proof), parsed_text ],"", 
         parsed_text_length 
   | TA.Check (_,term) ->
       let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
@@ -512,7 +528,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status
         let (_,menv,subst,_,_,_), _ = 
           ProofEngineTypes.apply_tactic
             (Auto.auto_tac ~dbd ~params
-              ~automation_cache:grafite_status.GrafiteTypes.automation_cache) 
+              ~automation_cache:grafite_status#automation_cache) 
             proof_status
         in
         let proof_term = 
@@ -581,9 +597,6 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff
 grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
 script ex loc
 =
- let module TAPp = GrafiteAstPp in
- let module MD = MultiPassDisambiguator in
- let module ML = MatitaMisc in
   try
    ignore (buffer#move_mark (`NAME "beginning_of_statement")
     ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
@@ -601,23 +614,26 @@ 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
 =
-  let (lexicon_status,st), unparsed_text =
+  let (grafite_status,st), unparsed_text =
     match statement with
     | `Raw text ->
         if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
         let ast = 
          wrap_with_make include_paths
           (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) 
-            (GrafiteTypes.get_estatus grafite_status)
+            grafite_status
         in
           ast, text
-    | `Ast (st, text) -> (GrafiteTypes.get_estatus grafite_status, st), text
+    | `Ast (st, text) -> (grafite_status, st), text
   in
-  let grafite_status = GrafiteTypes.set_estatus lexicon_status grafite_status in
   let text_of_loc floc = 
     let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
     let start, stop = HExtlib.loc_of_floc floc in 
@@ -632,6 +648,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.literate" *) ->
+     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
@@ -654,12 +679,6 @@ 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
@@ -802,7 +821,7 @@ object (self)
    buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext;
    (* here we need to set the Goal in case we are going to cursor (or to
       bottom) and we will face a macro *)
-   match self#grafite_status.proof_status with
+   match self#grafite_status#proof_status with
       Incomplete_proof p ->
        userGoal <-
          (try Some (Continuationals.Stack.find_goal p.stack)
@@ -815,9 +834,7 @@ object (self)
    let cur_grafite_status =
     match history with s::_ -> s | [] -> assert false
    in
-    LexiconSync.time_travel 
-      ~present:(GrafiteTypes.get_estatus cur_grafite_status)
-      ~past:(GrafiteTypes.get_estatus grafite_status);
+    LexiconSync.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;
@@ -984,9 +1001,7 @@ object (self)
     (* 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:(GrafiteTypes.get_estatus self#grafite_status)
-      ~past:(GrafiteTypes.get_estatus grafite_status)
+    LexiconSync.time_travel ~present:self#grafite_status ~past:grafite_status
 
   method private reset_buffer = 
     statements <- [];
@@ -1094,7 +1109,7 @@ object (self)
      HLog.error "The script is too big!\n"
   
   method onGoingProof () =
-    match self#grafite_status.proof_status with
+    match self#grafite_status#proof_status with
     | No_proof | Proof _ -> false
     | Incomplete_proof _ -> true
     | Intermediate _ -> assert false
@@ -1140,9 +1155,7 @@ object (self)
       | GrafiteParser.LNone _
       | GrafiteParser.LSome (GrafiteAst.Executable _) -> false
     in
-    try
-      is_there_only_comments 
-        (GrafiteTypes.get_estatus self#grafite_status) self#getFuture
+    try is_there_only_comments self#grafite_status self#getFuture
     with 
     | LexiconEngine.IncludedFileNotCompiled _
     | HExtlib.Localized _