Re: [isabelle] LaTeX document



On Friday 22 September 2006 11:32, Francisco Jose CHAVES ALONSO wrote:
> I need the TeX file generated by Isabelle, to extract some parts
> for another document that I also generate with another command.
> "isatool make" delete the TeX generated file. It is possible to
> save it?

I have a patch for Pure which does a few things, including this.

I've tried to snip out the relevant parts (thank heavens for 
diff-mode!), and attached the result.
It should apply against Isabelle 2005, but I haven't tested it.

(Note that I don't code in ML.  Do feel free to laugh at it.)

Once applied, you'd need to delete all your logic heaps and rebuild.
To prevent the tex files being cleaned up, you can then add something 
like:
  Present.no_clean := true;
to the ROOT.ML file for the relevant logic (I do so at the top).

Martin
diff -ur Isabelle2005.orig/src/Pure/Thy/present.ML Isabelle/src/Pure/Thy/present.ML
--- Isabelle2005.orig/src/Pure/Thy/present.ML	2005-09-20 07:24:37.000000000 +0100
+++ Isabelle/src/Pure/Thy/present.ML	2006-05-13 15:31:22.498249408 +0100
@@ -9,6 +9,7 @@
 sig
   val no_document: ('a -> 'b) -> 'a -> 'b
   val section: string -> unit
+  val no_clean: bool ref
 end;
 
 signature PRESENT =
@@ -169,6 +171,7 @@
 
 val suppress_tex_source = ref false;
 fun no_document f x = Library.setmp suppress_tex_source true f x;
+val no_clean = ref false;
 
 fun init_theory_info name info =
   change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
@@ -326,8 +330,9 @@
 
 fun isatool_document verbose format name tags path result_path =
   let
-    val s = "\"$ISATOOL\" document -c -o '" ^ format ^ "' \
+    val clean_opt = if !no_clean then "" else "-c"
+    val s = "\"$ISATOOL\" document " ^ clean_opt ^ " -o '" ^ format ^ "' \
       \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^
       " 2>&1" ^ (if verbose then "" else " >/dev/null");
     val doc_path = Path.append result_path (Path.ext format (Path.basic name));


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.