X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=5ddfb2b9c0a4c026aaffeb00ab8d73831c860b85;hb=8030b740ba0b84df1ae3a3e5878b447f3e4ec874;hp=891d09a50b20495e9c5da8f3c70d6f0d70792f68;hpb=5cb95a2e44f979183a8c3e39baa3b4e7cfaf8182;p=helm.git

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 891d09a50..5ddfb2b9c 100644
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -77,135 +77,110 @@ type guistuff = {
 }
 
 let eval_with_engine guistuff lexicon_status grafite_status user_goal
- parsed_text st
+ skipped_txt nonskipped_txt st
 =
   let module TAPp = GrafiteAstPp in
-  let parsed_text_length = String.length parsed_text in
-  let initial_space,parsed_text =
-   try
-    let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
-    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' =
-   (* the code commented out adds the "select" command if needed *)
-   initial_space,grafite_status,lexicon_status,[] in
-(* let loc, ex = 
-    match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
-    match grafite_status.proof_status with
-     | Incomplete_proof { stack = stack }
-      when not (List.mem user_goal (Continuationals.head_goals stack)) ->
-        let grafite_status =
-          MatitaEngine.eval_ast
-            ~do_heavy_checks:true grafite_status (goal_ast user_goal)
-        in
-        let initial_space = if initial_space = "" then "\n" else initial_space
-        in
-        "\n", grafite_status,
-        [ grafite_status,
-          initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ]
-      | _ -> initial_space,grafite_status,[] in *)
+  let module DTE = DisambiguateTypes.Environment in
+  let module DP = DisambiguatePp in
+  let parsed_text_length =
+    String.length skipped_txt + String.length nonskipped_txt 
+  in
+  let text = skipped_txt ^ nonskipped_txt in
+  let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in
   let enriched_history_fragment =
    MatitaEngine.eval_ast ~do_heavy_checks:true
-    new_lexicon_status new_grafite_status st
+    lexicon_status grafite_status (text,prefix_len,st)
   in
-  let _,new_text_list_rev = 
-    let module DTE = DisambiguateTypes.Environment in
-    let module UM = UriManager in
-    List.fold_right (
-      fun (_,alias) (initial_space,acc) ->
+  let enriched_history_fragment = List.rev enriched_history_fragment in
+  (* really fragile *)
+  let res,_ = 
+    List.fold_left 
+      (fun (acc, to_prepend) (status,alias) ->
        match alias with
-          None -> initial_space,initial_space::acc
-        | Some (k,((v,_) as value)) ->
-           let new_text =
-            let initial_space =
-             if initial_space = "" then "\n" else initial_space
-            in
-             initial_space ^
-              DisambiguatePp.pp_environment
-               (DisambiguateTypes.Environment.add k value
-                 DisambiguateTypes.Environment.empty)
-           in
-            "\n",new_text::acc
-    ) enriched_history_fragment (initial_space,[]) in
-  let new_text_list_rev =
-   match enriched_history_fragment,new_text_list_rev with
-      (_,None)::_, initial_space::tl -> (initial_space ^ parsed_text)::tl
-    | _,_ -> assert false
+       | None -> (status,to_prepend ^ nonskipped_txt)::acc,""
+       | Some (k,((v,_) as value)) ->
+            let newtxt = DP.pp_environment (DTE.add k value DTE.empty) in
+            (status,to_prepend ^ newtxt ^ "\n")::acc, "")
+      ([],skipped_txt) enriched_history_fragment
   in
-   let res =
-    try
-     List.combine (fst (List.split enriched_history_fragment)) new_text_list_rev
-    with
-     Invalid_argument _ -> assert false
-   in
-    res,parsed_text_length
+  res,parsed_text_length
 
 let wrap_with_developments guistuff f arg = 
+  let compile_needed_and_go_on lexiconfile d exc =
+    let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" lexiconfile in
+    let target = Pcre.replace ~pat:"metadata$" ~templ:"moo" target in
+    let refresh_cb () = 
+      while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
+    in
+    if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
+      raise exc
+    else
+      f arg
+  in
+  let do_nothing () = raise (ActionCancelled "Inclusion not performed") in
+  let check_if_file_is_exists f =
+    assert(Pcre.pmatch ~pat:"ma$" f);
+    let pwd = Sys.getcwd () in
+    let f_pwd = pwd ^ "/" ^ f in
+    if not (HExtlib.is_regular f_pwd) then
+      raise (ActionCancelled ("File "^f_pwd^" does not exists!"))
+    else
+      raise 
+        (ActionCancelled 
+          ("Internal error: "^f_pwd^" exists but I'm unable to include it!"))
+  in
+  let handle_with_devel d lexiconfile exc =
+    let name = MatitamakeLib.name_for_development d in
+    let title = "Unable to include " ^ lexiconfile in
+    let message = 
+      lexiconfile ^ " is handled by development <b>" ^ name ^ "</b>.\n\n" ^
+      "<i>Should I compile it and Its dependencies?</i>"
+    in
+    (match guistuff.ask_confirmation ~title ~message with
+    | `YES -> compile_needed_and_go_on lexiconfile d exc
+    | `NO -> raise exc
+    | `CANCEL -> do_nothing ())
+  in
+  let handle_without_devel mafilename exc =
+    let title = "Unable to include " ^ mafilename in
+    let message = 
+     mafilename ^ " is <b>not</b> handled by a development.\n" ^
+     "All dependencies are automatically solved for a development.\n\n" ^
+     "<i>Do you want to set up a development?</i>"
+    in
+    (match guistuff.ask_confirmation ~title ~message with
+    | `YES -> 
+        guistuff.develcreator ~containing:(Some (Filename.dirname mafilename));
+        do_nothing ()
+    | `NO -> raise exc
+    | `CANCEL -> do_nothing())
+  in
   try 
     f arg
   with
-  | DependenciesParser.UnableToInclude what 
-  | LexiconEngine.IncludedFileNotCompiled what 
-  | GrafiteEngine.IncludedFileNotCompiled what as exc ->
-      let compile_needed_and_go_on d =
-        let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" what in
-        let refresh_cb () = 
-          while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
-        in
-        if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
-          raise exc
-        else
-          f arg
-      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
-        let message = 
-          what ^ " is handled by development <b>" ^ name ^ "</b>.\n\n" ^
-          "<i>Should I compile it and Its dependencies?</i>"
-        in
-        (match guistuff.ask_confirmation ~title ~message with
-        | `YES -> compile_needed_and_go_on d
-        | `NO -> raise exc
-        | `CANCEL -> do_nothing ())
-      in
-      let handle_without_devel filename =
-        let title = "Unable to include " ^ what in
-        let message = 
-         what ^ " is <b>not</b> handled by a development.\n" ^
-         "All dependencies are automatically solved for a development.\n\n" ^
-         "<i>Do you want to set up a development?</i>"
-        in
-        (match guistuff.ask_confirmation ~title ~message with
-        | `YES -> 
-            (match filename with
-            | Some f -> 
-                guistuff.develcreator ~containing:(Some (Filename.dirname f))
-            | None -> guistuff.develcreator ~containing:None);
-            do_nothing ()
-        | `NO -> raise exc
-        | `CANCEL -> do_nothing())
-      in
-      match guistuff.filenamedata with
-      | None,None -> handle_without_devel None
-      | None,Some d -> handle_with_devel d
-      | Some f,_ ->
-          match MatitamakeLib.development_for_dir (Filename.dirname f) with
-          | None -> handle_without_devel (Some f)
-          | Some d -> handle_with_devel d
+  | DependenciesParser.UnableToInclude mafilename -> 
+      assert (Pcre.pmatch ~pat:"ma$" mafilename);
+      check_if_file_is_exists mafilename
+  | LexiconEngine.IncludedFileNotCompiled (xfilename,mafilename) 
+  | GrafiteEngine.IncludedFileNotCompiled (xfilename,mafilename) as exn ->
+      assert (Pcre.pmatch ~pat:"ma$" mafilename);
+      assert (Pcre.pmatch ~pat:"lexicon$" xfilename || 
+              Pcre.pmatch ~pat:"mo$" xfilename );
+      (* we know that someone was able to include the .ma, get the baseuri
+       * but was unable to get the compilation output 'xfilename' *)
+      match MatitamakeLib.development_for_dir (Filename.dirname mafilename) with
+      | None -> handle_without_devel mafilename exn
+      | Some d -> handle_with_devel d xfilename exn
 ;;
     
 let eval_with_engine
-     guistuff lexicon_status grafite_status user_goal parsed_text st
+     guistuff lexicon_status grafite_status user_goal 
+       skipped_txt nonskipped_txt st
 =
   wrap_with_developments guistuff
     (eval_with_engine 
-      guistuff lexicon_status grafite_status user_goal parsed_text) st
+      guistuff lexicon_status grafite_status user_goal 
+        skipped_txt nonskipped_txt) st
 ;;
 
 let pp_eager_statement_ast =
@@ -221,27 +196,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) ->
@@ -251,13 +230,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 *)
@@ -283,7 +262,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
           let text =
            comment parsed_text ^ "\n" ^
             pp_eager_statement_ast (ast HExtlib.dummy_floc) in
-          let text_len = String.length text in
+          let text_len = MatitaGtkMisc.utf8_string_length text in
           let loc = HExtlib.floc_of_loc (0,text_len) in
           let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
           let res,_parsed_text_len =
@@ -309,13 +288,10 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
       let t_and_ty = Cic.Cast (term,ty) in
       guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
       [], parsed_text_length
-  (* TODO *)
-  | TA.Quit _ -> failwith "not implemented"
-  | TA.Print (_,kind) -> failwith "not implemented"
-  | TA.Search_pat (_, search_kind, str) -> failwith "not implemented"
-  | TA.Search_term (_, search_kind, term) -> failwith "not implemented"
                                 
-and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script loc ex
+and eval_executable include_paths (buffer : GText.buffer) guistuff
+lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
+script ex loc
 =
  let module TAPp = GrafiteAstPp in
  let module MD = GrafiteDisambiguator in
@@ -341,7 +317,7 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_statu
      | _ -> ()
    end;
    eval_with_engine
-    guistuff lexicon_status grafite_status user_goal parsed_text
+    guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt
      (TA.Executable (loc, ex))
   with
      MatitaTypes.Cancel -> [], 0
@@ -352,7 +328,7 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_statu
         | Some n -> GrafiteTypes.get_proof_context grafite_status n in
       let grafite_status,macro = lazy_macro context in
        eval_macro include_paths buffer guistuff lexicon_status grafite_status
-        user_goal unparsed_text parsed_text script macro
+        user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
 
 and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
  grafite_status user_goal script statement
@@ -369,18 +345,22 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
           ast, text
     | `Ast (st, text) -> (lexicon_status, st), text
   in
-  let text_of_loc loc =
-    let parsed_text_length = snd (HExtlib.loc_of_floc loc) in
-    let parsed_text = safe_substring unparsed_text 0 parsed_text_length in
-    parsed_text, parsed_text_length
-  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 
+    let floc = HExtlib.floc_of_loc (0, start) in
+    let skipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
+    let floc = HExtlib.floc_of_loc (0, stop) in
+    let txt,len = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
+    txt,nonskipped_txt,skipped_txt,len
+  in 
   match st with
   | GrafiteParser.LNone loc ->
-      let parsed_text, parsed_text_length = text_of_loc loc in
+      let parsed_text, _, _, parsed_text_length = text_of_loc loc in
        [(grafite_status,lexicon_status),parsed_text],
         parsed_text_length
   | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> 
-      let parsed_text, parsed_text_length = text_of_loc loc in
+      let parsed_text, _, _, parsed_text_length = text_of_loc loc in
       let remain_len = String.length unparsed_text - parsed_text_length in
       let s = String.sub unparsed_text parsed_text_length remain_len in
       let s,len = 
@@ -389,7 +369,8 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
          grafite_status user_goal script (`Raw s)
        with
           HExtlib.Localized (floc, exn) ->
-           HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn
+           HExtlib.raise_localized_exception 
+             ~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn
         | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
            raise
             (GrafiteDisambiguator.DisambiguationError
@@ -400,9 +381,11 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
          (statuses,parsed_text ^ text)::tl,parsed_text_length + len
       | [] -> [], 0)
   | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
-     let parsed_text, parsed_text_length = text_of_loc loc in
+     let _, nonskipped, skipped, parsed_text_length = 
+       text_of_loc loc 
+     in
       eval_executable include_paths buffer guistuff lexicon_status
-       grafite_status user_goal unparsed_text parsed_text script loc ex
+       grafite_status user_goal unparsed_text skipped nonskipped script ex loc
   
 let fresh_script_id =
   let i = ref 0 in
@@ -502,12 +485,14 @@ object (self)
    if statement <> None then
      buffer#insert ~iter:start new_text
    else begin
-     if new_text <> String.sub s 0 parsed_len then begin
-       buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len);
+     let parsed_text = String.sub s 0 parsed_len in
+     if new_text <> parsed_text then begin
+       let stop = start#copy#forward_chars (Glib.Utf8.length parsed_text) in
+       buffer#delete ~start ~stop;
        buffer#insert ~iter:start new_text;
      end;
    end;
-   self#moveMark (String.length new_text);
+   self#moveMark (Glib.Utf8.length  new_text);
    (* 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
@@ -535,6 +520,7 @@ object (self)
       self#notify
     with 
     | Margin -> self#notify
+    | Not_found -> assert false
     | exc -> self#notify; raise exc
 
   method retract () =
@@ -542,7 +528,8 @@ object (self)
       let cmp,new_statements,new_history,(grafite_status,lexicon_status) =
        match statements,history with
           stat::statements, _::(status::_ as history) ->
-           String.length stat, statements, history, status
+           assert (Glib.Utf8.validate stat);
+           Glib.Utf8.length stat, statements, history, status
        | [],[_] -> raise Margin
        | _,_ -> assert false
       in
@@ -596,6 +583,11 @@ object (self)
     let grafite_status = self#grafite_status in
     List.iter (fun o -> o lexicon_status grafite_status) observers
 
+  method loadFromString s =
+    buffer#set_text s;
+    self#reset_buffer;
+    buffer#set_modified true
+
   method loadFromFile f =
     buffer#set_text (HExtlib.input_file f);
     self#reset_buffer;
@@ -740,7 +732,7 @@ object (self)
              self#_retract (icmp - len) lexicon_status grafite_status statements
               history
           | statement::tl1, _::tl2 ->
-             back_until_cursor (len - String.length statement) (tl1,tl2)
+             back_until_cursor (len - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2)
           | _,_ -> assert false
         in
         (try
@@ -784,7 +776,6 @@ object (self)
   method goal = userGoal
 
   method eos = 
-    let s = self#getFuture in
     let rec is_there_only_comments lexicon_status s = 
       if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
       let lexicon_status,st =
@@ -793,7 +784,10 @@ object (self)
       in
       match st with
       | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> 
-          let parsed_text_length = snd (HExtlib.loc_of_floc loc) in
+          let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
+          (* CSC: why +1 in the following lines ???? *)
+          let parsed_text_length = parsed_text_length + 1 in
+prerr_endline ("## " ^ string_of_int parsed_text_length);
           let remain_len = String.length s - parsed_text_length in
           let next = String.sub s parsed_text_length remain_len in
           is_there_only_comments lexicon_status next
@@ -801,8 +795,9 @@ object (self)
       | GrafiteParser.LSome (GrafiteAst.Executable _) -> false
     in
     try
-      is_there_only_comments self#lexicon_status s
+      is_there_only_comments self#lexicon_status self#getFuture
     with 
+    | LexiconEngine.IncludedFileNotCompiled _
     | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true