X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=9eb1dbf69c608c9ba231d4e46f45f3ae78fb1f18;hb=5abe94a6813fc8fc810df6a35bdb32eaac179536;hp=f124bd5c922fc231603a3df848ab1d07be5992aa;hpb=3ef63c09695a55d3da601a554441b8a69daf54a9;p=helm.git

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index f124bd5c9..9eb1dbf69 100644
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -60,14 +60,6 @@ let first_line s =
     String.sub s 0 nl_pos
   with Not_found -> s
 
-  (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
-let goal_ast n =
-  let module A = GrafiteAst in
-  let loc = HExtlib.dummy_floc in
-  A.Executable (loc, A.Tactical (loc,
-    A.Tactic (loc, A.Goal (loc, n)),
-    Some (A.Dot loc)))
-
 type guistuff = {
   mathviewer:MatitaTypes.mathViewer;
   urichooser: UriManager.uri list -> UriManager.uri list;
@@ -255,10 +247,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
       | [uri] -> 
           let suri = UriManager.string_of_uri uri in
           let ast loc =
-            TA.Executable (loc, (TA.Tactical (loc,
-              TA.Tactic (loc,
-                TA.Apply (loc, CicNotationPt.Uri (suri, None))),
-                Some (TA.Dot loc)))) in
+            TA.Executable (loc, (TA.Tactic (loc,
+             Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
+             TA.Dot loc))) in
           let text =
            comment parsed_text ^ "\n" ^
             pp_eager_statement_ast (ast HExtlib.dummy_floc) in
@@ -289,54 +280,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 "\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
+       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