Added is_trans_eq_URI and is_sym_eq_URI

[helm.git] / matita / matitaScript.ml

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 62d760c3b993b365b01b133b362855b3a3b20324..b853ddd4e76cdf93eaee7a504432f7d5962012a0 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -101,8 +101,6 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
             (status,to_prepend ^ newtxt ^ "\n")::acc, "")
       ([],skipped_txt) enriched_history_fragment
   in
-  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 = 
@@ -362,7 +360,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
@@ -719,7 +718,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