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

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 7a978bbde..8ab94d979 100644
--- a/matita/matitaScript.ml
+++ b/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;
@@ -289,54 +289,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
       guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
       [], "", parsed_text_length
   | TA.Inline (_,style,suri,prefix) ->
-     let dbd = LibraryDb.instance () in
-     let uris =
-      let sql_pat =
-       (Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" suri) ^ "%" in
-      let query =
-       sprintf ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^
-                "SELECT source FROM %s WHERE source LIKE \"%s\"")
-         (MetadataTypes.name_tbl ()) sql_pat
-         MetadataTypes.library_name_tbl sql_pat in
-      let result = HMysql.exec dbd query in
-       HMysql.map result
-        (function cols ->
-          match cols.(0) with
-             Some s -> UriManager.uri_of_string s
-           | _ -> assert false)
-     in
-prerr_endline "Inizio sorting";
-      let sorted_uris = MetadataDeps.topological_sort ~dbd uris in
-prerr_endline "Fine sorting";
-      let sorted_uris_without_xpointer =
-       HExtlib.filter_map
-        (function uri ->
-          let s =
-           Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:""
-            (UriManager.string_of_uri uri) in
-          try
-           ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s);
-           None
-          with
-           Not_found ->
-            Some (UriManager.uri_of_string s)
-        ) sorted_uris
-      in
-      let declarative =
-       String.concat "\n\n"
-        (List.map
-          (fun uri ->
-prerr_endline ("Stampo " ^ UriManager.string_of_uri uri);
-            try
-             ObjPp.obj_to_string 78 style prefix (* FG: mi pare meglio 78 *)
-              (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
-            with
-	     | 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
+       let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+       [], str, String.length parsed_text
                                 
 and eval_executable include_paths (buffer : GText.buffer) guistuff
 lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
@@ -578,6 +532,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 () =
@@ -595,6 +550,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 =
@@ -728,6 +684,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"
@@ -807,7 +764,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
@@ -858,6 +817,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 () =