]> matita.cs.unibo.it Git - helm.git/commitdiff
to tired to write a message.
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 13 Apr 2006 23:44:51 +0000 (23:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 13 Apr 2006 23:44:51 +0000 (23:44 +0000)
matita/.depend
matita/Makefile
matita/matitaEngine.ml
matita/matitaExcPp.ml
matita/matitaGtkMisc.ml
matita/matitaGtkMisc.mli
matita/matitaScript.ml

index 576d9dee8a2c0b0fc8d308aa0f6e6b5a7f2d04cd..2c41ea6ef92fc70c88c9941ea568ea83dbda2654 100644 (file)
@@ -22,8 +22,10 @@ matitaEngine.cmo: matitaEngine.cmi
 matitaEngine.cmx: matitaEngine.cmi 
 matitaExcPp.cmo: matitaExcPp.cmi 
 matitaExcPp.cmx: matitaExcPp.cmi 
-matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo matitaGtkMisc.cmi 
-matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi 
+matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmi \
+    matitaGtkMisc.cmi 
+matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
+    matitaGtkMisc.cmi 
 matitaGui.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi \
     matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \
     matitaGeneratedGui.cmo matitaExcPp.cmi buildTimeConf.cmi matitaGui.cmi 
@@ -49,11 +51,11 @@ matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \
 matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \
     matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx 
 matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \
-    matitaEngine.cmi buildTimeConf.cmi applyTransformation.cmi \
-    matitaScript.cmi 
+    matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmi \
+    applyTransformation.cmi matitaScript.cmi 
 matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \
-    matitaEngine.cmx buildTimeConf.cmx applyTransformation.cmx \
-    matitaScript.cmi 
+    matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \
+    applyTransformation.cmx matitaScript.cmi 
 matitaTypes.cmo: matitaTypes.cmi 
 matitaTypes.cmx: matitaTypes.cmi 
 matitaGtkMisc.cmi: matitaGeneratedGui.cmo 
index b9755831a1d729bd41b396521a40f18c5b084479..af7445047186cbf590325ad5af54d2760ef6bd63 100644 (file)
@@ -35,9 +35,9 @@ CMOS =                                \
        matitaEngine.cmo        \
        matitacLib.cmo          \
        applyTransformation.cmo \
+       matitaGtkMisc.cmo       \
        matitaScript.cmo        \
        matitaGeneratedGui.cmo  \
-       matitaGtkMisc.cmo       \
        matitaMathView.cmo      \
        matitaGui.cmo           \
        $(NULL)
@@ -110,6 +110,8 @@ links:
                        $(INSTALL_PROGRAMS_LINKS_MATITA); do\
                ln -sf $$X.opt $$X;\
        done
+       $(H)ln -sf matita.opt matita
+       $(H)ln -sf matitac.opt matitac
 
 matita: matita.ml $(LIB_DEPS) $(CMOS)
        $(H)echo "  OCAMLC $<"
index f0d8ee46c7820b34feff186135edcd418b9b4fd4..18022691cd27c953bf8a9b3a49bfc0611e80d3f5 100644 (file)
@@ -93,7 +93,7 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
         LexiconEngine.set_proof_aliases lexicon_status [k,value]
        in
         new_lexicon_status,
-         ((new_grafite_status,new_lexicon_status),Some (k,value))::acc
+         ((grafite_status,new_lexicon_status),Some (k,value))::acc
    ) (lexicon_status,[]) new_aliases
  in
   ((new_grafite_status,new_lexicon_status),None)::intermediate_states
index ed0be49564d641e53743df560a337e7bf0e9181c..24608be42260bdb5bc3d3c2018b5af7eb9268283 100644 (file)
@@ -62,6 +62,8 @@ let rec to_string =
      None, "Type checking assertion failed: " ^ Lazy.force msg
   | LibrarySync.AlreadyDefined s -> 
      None, "Already defined: " ^ UriManager.string_of_uri s
+  | CoercDb.EqCarrNotImplemented msg ->
+     None, ("EqCarrNotImplemented: " ^ Lazy.force msg)
   | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
      let rec aux n ?(dummy=false) (prev_msg,phases) =
       function
index a41dbffe373713d3ca3fa5858e215f801afe5a58..c397215a790d20e78510d5eb80b26cb3543bc7cf 100644 (file)
@@ -439,3 +439,15 @@ let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "")
   GtkThread.main ();
   (match !record_no with Some n -> n | _ -> raise MatitaTypes.Cancel)
 
+let utf8_parsed_text s floc = 
+  let start, stop = HExtlib.loc_of_floc floc in
+  let start_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:start in
+  let stop_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:stop in
+  let bytes = stop_bytes - start_bytes in
+  String.sub s start_bytes bytes, bytes
+  
+let utf8_string_length s = 
+  if BuildTimeConf.debug then
+    assert(Glib.Utf8.validate s);
+  Glib.Utf8.length s
+    
index 1affd2a39e78822d2449ef7abe087d57102b4717..16b0591b2651a5a09856f5bdfad0c192c66d9c58 100644 (file)
@@ -155,3 +155,11 @@ val report_error:
   unit ->
     unit
 
+    (* given an utf8 string a floc returns the parsed substring and its length
+     * in bytes *)
+val utf8_parsed_text: string -> Token.flocation -> string * int
+
+    (* the length in characters, not bytes *)
+val utf8_string_length: string -> int
+
+
index 4c40f9e14588686c9f9d879ab1721658b432eff3..62d760c3b993b365b01b133b362855b3a3b20324 100644 (file)
@@ -77,72 +77,33 @@ 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 enriched_history_fragment =
    MatitaEngine.eval_ast ~do_heavy_checks:true
-    new_lexicon_status new_grafite_status st
+    lexicon_status grafite_status 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
+  let res = (*List.combine (List.map fst (List.rev enriched_history_fragment))
+  strings*) res in 
+  res,parsed_text_length
 
 let wrap_with_developments guistuff f arg = 
   try 
@@ -201,11 +162,13 @@ let wrap_with_developments guistuff f arg =
 ;;
     
 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 =
@@ -287,7 +250,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 =
@@ -319,7 +282,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
   | 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
@@ -345,7 +310,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
@@ -356,7 +321,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
@@ -373,18 +338,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 = 
@@ -404,9 +373,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
@@ -506,12 +477,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
@@ -547,7 +520,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
@@ -789,7 +763,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 =
@@ -798,7 +771,9 @@ 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
           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
@@ -806,7 +781,7 @@ 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 
     | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false