ML_idf antiquotation
authorhaftmann
Tue May 24 14:28:59 2005 +0200 (2005-05-24)
changeset 160647953879aa6cf
parent 16063 7dd4eb2c8055
child 16065 8665446944ce
ML_idf antiquotation
Admin/page/dist-content/isabelle_macos_screenshot.jpg
doc-src/LaTeXsugar/Sugar/Sugar.thy
lib/Tools/latex
lib/texinputs/draft.tex
lib/texinputs/isabelle.sty
lib/texinputs/isabellesym.sty
lib/texinputs/pdfsetup.sty
src/Pure/Isar/isar_output.ML
     1.1 Binary file Admin/page/dist-content/isabelle_macos_screenshot.jpg has changed
     2.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 24 11:19:50 2005 +0200
     2.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 24 14:28:59 2005 +0200
     2.3 @@ -372,7 +372,7 @@
     2.4    style has some object-logic specific behaviour).
     2.5  
     2.6    The mapping from identifier name to the style function
     2.7 -  is done by the \verb!Style.add_style! expression which expects the desired
     2.8 +  is done by the @{ML_idf TermStyle.add_style} expression which expects the desired
     2.9    style name and the style function as arguments.
    2.10    
    2.11    After this \verb!setup!,
     3.1 --- a/lib/Tools/latex	Tue May 24 11:19:50 2005 +0200
     3.2 +++ b/lib/Tools/latex	Tue May 24 14:28:59 2005 +0200
     3.3 @@ -81,7 +81,11 @@
     3.4  function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
     3.5  function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
     3.6  function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
     3.7 -function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
     3.8 +function copy_styles ()
     3.9 +{
    3.10 +  cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR";
    3.11 +  "$AUTO_PERL" -n -i -e 's/\$Id(?::\s)*([^\$]*)\$/originating from CVS: $1/g; print;' "$DIR"/*.sty
    3.12 +}
    3.13  
    3.14  function extract_syms ()
    3.15  {
     4.1 --- a/lib/texinputs/draft.tex	Tue May 24 11:19:50 2005 +0200
     4.2 +++ b/lib/texinputs/draft.tex	Tue May 24 14:28:59 2005 +0200
     4.3 @@ -4,6 +4,7 @@
     4.4  %% root for draft documents
     4.5  %%
     4.6  
     4.7 +
     4.8  \documentclass[10pt,a4paper]{article}
     4.9  \usepackage{isabelle,isabellesym,pdfsetup}
    4.10  
     5.1 --- a/lib/texinputs/isabelle.sty	Tue May 24 11:19:50 2005 +0200
     5.2 +++ b/lib/texinputs/isabelle.sty	Tue May 24 14:28:59 2005 +0200
     5.3 @@ -3,6 +3,7 @@
     5.4  %%
     5.5  %% macros for Isabelle generated LaTeX output
     5.6  %%
     5.7 +%% $Id$
     5.8  
     5.9  %%% Simple document preparation (based on theory token language and symbols)
    5.10  
     6.1 --- a/lib/texinputs/isabellesym.sty	Tue May 24 11:19:50 2005 +0200
     6.2 +++ b/lib/texinputs/isabellesym.sty	Tue May 24 14:28:59 2005 +0200
     6.3 @@ -3,6 +3,7 @@
     6.4  %%
     6.5  %% definitions of standard Isabelle symbols
     6.6  %%
     6.7 +%% $Id$
     6.8  
     6.9  % symbol definitions
    6.10  
     7.1 --- a/lib/texinputs/pdfsetup.sty	Tue May 24 11:19:50 2005 +0200
     7.2 +++ b/lib/texinputs/pdfsetup.sty	Tue May 24 14:28:59 2005 +0200
     7.3 @@ -3,6 +3,7 @@
     7.4  %%
     7.5  %% smart url or hyperref setup
     7.6  %%
     7.7 +%% $Id$
     7.8  
     7.9  \@ifundefined{pdfoutput}
    7.10  {\usepackage{url}}
     8.1 --- a/src/Pure/Isar/isar_output.ML	Tue May 24 11:19:50 2005 +0200
     8.2 +++ b/src/Pure/Isar/isar_output.ML	Tue May 24 14:28:59 2005 +0200
     8.3 @@ -386,6 +386,10 @@
     8.4    Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state
     8.5        handle Toplevel.UNDEF => error "No proof state")))) src state;
     8.6  
     8.7 +(*this is just experimental*)
     8.8 +fun output_ml_idf src ctxt idf = snd (use_text Context.ml_output true idf,
     8.9 +    output_with (K pretty_text) src ctxt idf);
    8.10 +
    8.11  val _ = add_commands
    8.12   [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
    8.13    ("thm_style", args ((Scan.lift Args.name) -- Attrib.local_thm) (output_with pretty_thm_style)),
    8.14 @@ -400,6 +404,8 @@
    8.15    ("goals", output_goals true),
    8.16    ("subgoals", output_goals false),
    8.17    ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
    8.18 -  ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))];
    8.19 +  ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))),
    8.20 +  (*this is just experimental*)
    8.21 +  ("ML_idf", args (Scan.lift Args.name) output_ml_idf)];
    8.22  
    8.23  end;