methods eos, goto, advance and retract now catch Invalid_argument "Array.make"

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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 12f26036b4a1c20f829090e6ee254f74ed964f0d..f124bd5c922fc231603a3df848ab1d07be5992aa 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -234,7 +234,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
      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 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 mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
@@ -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,prefix) ->
+  | 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 "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
+               (UriManager.string_of_uri uri) (Printexc.to_string e)
           ) sorted_uris_without_xpointer)
       in
        [],declarative,String.length parsed_text
@@ -576,6 +578,7 @@ object (self)
     with 
     | Margin -> self#notify
     | Not_found -> assert false
+    | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n"
     | exc -> self#notify; raise exc
 
   method retract () =
@@ -593,6 +596,7 @@ object (self)
        self#notify
     with 
     | Margin -> self#notify
+    | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n"
     | exc -> self#notify; raise exc
 
   method private getFuture =
@@ -726,6 +730,7 @@ object (self)
      set_star (Filename.basename self#ppFilename) false
 
   method goto (pos: [`Top | `Bottom | `Cursor]) () =
+  try  
     let old_locked_mark =
      `MARK
        (buffer#create_mark ~name:"old_locked_mark"
@@ -805,7 +810,9 @@ object (self)
         | Margin -> dispose_remember (); dispose_old_locked_mark (); self#notify
         | exc -> dispose_remember (); dispose_old_locked_mark ();
                  self#notify; raise exc)
-              
+  with Invalid_argument "Array.make" ->
+     HLog.error "The script is too big!\n"
+  
   method onGoingProof () =
     match self#grafite_status.proof_status with
     | No_proof | Proof _ -> false
@@ -856,6 +863,7 @@ prerr_endline ("## " ^ string_of_int parsed_text_length);
     | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true
+    | Invalid_argument "Array.make" -> false
 
   (* debug *)
   method dump () =