# HG changeset patch
# User haftmann
# Date 1116937739 -7200
# Node ID 7953879aa6cf6eae9ff021063a6c187f17bad238
# Parent  7dd4eb2c8055a1d92f6d8dd88d106ee6995a1a81
ML_idf antiquotation

diff -r 7dd4eb2c8055 -r 7953879aa6cf Admin/page/dist-content/isabelle_macos_screenshot.jpg
Binary file Admin/page/dist-content/isabelle_macos_screenshot.jpg has changed
diff -r 7dd4eb2c8055 -r 7953879aa6cf doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 24 11:19:50 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 24 14:28:59 2005 +0200
@@ -372,7 +372,7 @@
   style has some object-logic specific behaviour).
 
   The mapping from identifier name to the style function
-  is done by the \verb!Style.add_style! expression which expects the desired
+  is done by the @{ML_idf TermStyle.add_style} expression which expects the desired
   style name and the style function as arguments.
   
   After this \verb!setup!,
diff -r 7dd4eb2c8055 -r 7953879aa6cf lib/Tools/latex
--- a/lib/Tools/latex	Tue May 24 11:19:50 2005 +0200
+++ b/lib/Tools/latex	Tue May 24 14:28:59 2005 +0200
@@ -81,7 +81,11 @@
 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
-function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
+function copy_styles ()
+{
+  cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR";
+  "$AUTO_PERL" -n -i -e 's/\$Id(?::\s)*([^\$]*)\$/originating from CVS: $1/g; print;' "$DIR"/*.sty
+}
 
 function extract_syms ()
 {
diff -r 7dd4eb2c8055 -r 7953879aa6cf lib/texinputs/draft.tex
--- a/lib/texinputs/draft.tex	Tue May 24 11:19:50 2005 +0200
+++ b/lib/texinputs/draft.tex	Tue May 24 14:28:59 2005 +0200
@@ -4,6 +4,7 @@
 %% root for draft documents
 %%
 
+
 \documentclass[10pt,a4paper]{article}
 \usepackage{isabelle,isabellesym,pdfsetup}
 
diff -r 7dd4eb2c8055 -r 7953879aa6cf lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Tue May 24 11:19:50 2005 +0200
+++ b/lib/texinputs/isabelle.sty	Tue May 24 14:28:59 2005 +0200
@@ -3,6 +3,7 @@
 %%
 %% macros for Isabelle generated LaTeX output
 %%
+%% $Id$
 
 %%% Simple document preparation (based on theory token language and symbols)
 
diff -r 7dd4eb2c8055 -r 7953879aa6cf lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Tue May 24 11:19:50 2005 +0200
+++ b/lib/texinputs/isabellesym.sty	Tue May 24 14:28:59 2005 +0200
@@ -3,6 +3,7 @@
 %%
 %% definitions of standard Isabelle symbols
 %%
+%% $Id$
 
 % symbol definitions
 
diff -r 7dd4eb2c8055 -r 7953879aa6cf lib/texinputs/pdfsetup.sty
--- a/lib/texinputs/pdfsetup.sty	Tue May 24 11:19:50 2005 +0200
+++ b/lib/texinputs/pdfsetup.sty	Tue May 24 14:28:59 2005 +0200
@@ -3,6 +3,7 @@
 %%
 %% smart url or hyperref setup
 %%
+%% $Id$
 
 \@ifundefined{pdfoutput}
 {\usepackage{url}}
diff -r 7dd4eb2c8055 -r 7953879aa6cf src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Tue May 24 11:19:50 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML	Tue May 24 14:28:59 2005 +0200
@@ -386,6 +386,10 @@
   Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state
       handle Toplevel.UNDEF => error "No proof state")))) src state;
 
+(*this is just experimental*)
+fun output_ml_idf src ctxt idf = snd (use_text Context.ml_output true idf,
+    output_with (K pretty_text) src ctxt idf);
+
 val _ = add_commands
  [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
   ("thm_style", args ((Scan.lift Args.name) -- Attrib.local_thm) (output_with pretty_thm_style)),
@@ -400,6 +404,8 @@
   ("goals", output_goals true),
   ("subgoals", output_goals false),
   ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
-  ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))];
+  ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))),
+  (*this is just experimental*)
+  ("ML_idf", args (Scan.lift Args.name) output_ml_idf)];
 
 end;