types2006 patch

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index b853ddd4e76cdf93eaee7a504432f7d5962012a0..07a7cbd2ed553a8b736fb83299d45c2c8cbeac57 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -85,9 +85,11 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
   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
-    lexicon_status grafite_status st
+    lexicon_status grafite_status (text,prefix_len,st)
   in
   let enriched_history_fragment = List.rev enriched_history_fragment in
   (* really fragile *)