X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=7a978bbde3bb19fdd2d0b6eb7d1de28fa17b0831;hb=8d04559d1b190e74e1d560000b01a648d086f484;hp=23de391c6ed37e486d1b0324f429325a41d98af4;hpb=afea2be14c1c197e0804e8607fc6dcc49ce46955;p=helm.git

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 23de391c6..7a978bbde 100644
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -288,7 +288,7 @@ 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
-  | TA.Inline (_,suri) ->
+  | TA.Inline (_,style,suri,prefix) ->
      let dbd = LibraryDb.instance () in
      let uris =
       let sql_pat =
@@ -328,10 +328,12 @@ prerr_endline "Fine sorting";
           (fun uri ->
 prerr_endline ("Stampo " ^ UriManager.string_of_uri uri);
             try
-             ObjPp.obj_to_string 80
+             ObjPp.obj_to_string 78 style prefix (* FG: mi pare meglio 78 *)
               (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
             with
-             _ (* BRRRRRRRRR *) -> "ERRORE IN STAMPA DI " ^ UriManager.string_of_uri uri
+	     | e (* BRRRRRRRRR *) -> 
+	        Printf.sprintf "\nERRORE IN STAMPA DI %s\n%s\n" 
+		(UriManager.string_of_uri uri) (Printexc.to_string e)
           ) sorted_uris_without_xpointer)
       in
        [],declarative,String.length parsed_text
@@ -363,6 +365,9 @@ script ex loc
            | `CANCEL -> raise MatitaTypes.Cancel)
      | _ -> ()
    end;
+   ignore (buffer#move_mark (`NAME "beginning_of_statement")
+    ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
+       (Glib.Utf8.length skipped_txt))) ;
    eval_with_engine
     guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt
      (TA.Executable (loc, ex))
@@ -501,6 +506,9 @@ object (self)
   (** text mark and tag representing locked part of a script *)
   val locked_mark =
     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
+  val beginning_of_statement_mark =
+    buffer#create_mark ~name:"beginning_of_statement"
+     ~left_gravity:true buffer#start_iter
   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
   val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]