--- a/NEWS Mon Oct 20 16:12:23 2014 +0100
+++ b/NEWS Mon Oct 20 17:41:04 2014 +0200
@@ -146,6 +146,17 @@
argument. Minor INCOMPATIBILITY.
+*** Document preparation ***
+
+* Official support for "tt" style variants, via \isatt{...} or
+\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
+verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
+as argument to other macros (such as footnotes).
+
+* Document antiquotation @{verbatim} prints ASCII text literally in "tt"
+style.
+
+
*** ML ***
* Tactical PARALLEL_ALLGOALS is the most common way to refer to
--- a/lib/texinputs/isabelle.sty Mon Oct 20 16:12:23 2014 +0100
+++ b/lib/texinputs/isabelle.sty Mon Oct 20 17:41:04 2014 +0200
@@ -9,7 +9,9 @@
\newcommand{\isabellecontext}{UNKNOWN}
\newcommand{\isastyle}{\UNDEF}
+\newcommand{\isastylett}{\UNDEF}
\newcommand{\isastyleminor}{\UNDEF}
+\newcommand{\isastyleminortt}{\UNDEF}
\newcommand{\isastylescript}{\UNDEF}
\newcommand{\isastyletext}{\normalsize\rm}
\newcommand{\isastyletxt}{\rm}
@@ -46,11 +48,22 @@
\isa@parskip\parskip\parskip0pt%
\isaspacing\isastyle}{\par}
+\newenvironment{isabellebodytt}{%
+\isamarkuptrue\par%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isaspacing\isastylett}{\par}
+
\newenvironment{isabelle}
{\begin{trivlist}\begin{isabellebody}\item\relax}
{\end{isabellebody}\end{trivlist}}
+\newenvironment{isabellett}
+{\begin{trivlist}\begin{isabellebodytt}\item\relax}
+{\end{isabellebodytt}\end{trivlist}}
+
\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
+\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
\newcommand{\isaindent}[1]{\hphantom{#1}}
\newcommand{\isanewline}{\mbox{}\par\mbox{}}
@@ -133,7 +146,9 @@
\newcommand{\isabellestyledefault}{%
\def\isastyle{\small\tt\slshape}%
+\def\isastylett{\small\tt}%
\def\isastyleminor{\small\tt\slshape}%
+\def\isastyleminortt{\small\tt}%
\def\isastylescript{\footnotesize\tt\slshape}%
\isachardefaults%
}
@@ -141,14 +156,18 @@
\newcommand{\isabellestylett}{%
\def\isastyle{\small\tt}%
+\def\isastylett{\small\tt}%
\def\isastyleminor{\small\tt}%
+\def\isastyleminortt{\small\tt}%
\def\isastylescript{\footnotesize\tt}%
\isachardefaults%
}
\newcommand{\isabellestyleit}{%
\def\isastyle{\small\it}%
+\def\isastylett{\small\tt}%
\def\isastyleminor{\it}%
+\def\isastyleminortt{\tt}%
\def\isastylescript{\footnotesize\it}%
\isachardefaults%
\def\isacharunderscorekeyword{\mbox{-}}%
@@ -206,7 +225,9 @@
\newcommand{\isabellestylesl}{%
\isabellestyleit%
\def\isastyle{\small\sl}%
+\def\isastylett{\small\tt}%
\def\isastyleminor{\sl}%
+\def\isastyleminortt{\tt}%
\def\isastylescript{\footnotesize\sl}%
}
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Mon Oct 20 16:12:23 2014 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Mon Oct 20 17:41:04 2014 +0200
@@ -125,6 +125,7 @@
@{antiquotation_def ML_type} & : & @{text antiquotation} \\
@{antiquotation_def ML_structure} & : & @{text antiquotation} \\
@{antiquotation_def ML_functor} & : & @{text antiquotation} \\
+ @{antiquotation_def verbatim} & : & @{text antiquotation} \\
@{antiquotation_def "file"} & : & @{text antiquotation} \\
@{antiquotation_def "url"} & : & @{text antiquotation} \\
@{antiquotation_def "cite"} & : & @{text antiquotation} \\
@@ -179,6 +180,7 @@
@@{antiquotation ML_type} options @{syntax text} |
@@{antiquotation ML_structure} options @{syntax text} |
@@{antiquotation ML_functor} options @{syntax text} |
+ @@{antiquotation verbatim} options @{syntax text} |
@@{antiquotation "file"} options @{syntax name} |
@@{antiquotation file_unchecked} options @{syntax name} |
@@{antiquotation url} options @{syntax name} |
@@ -271,6 +273,9 @@
check text @{text s} as ML value, infix operator, type, structure,
and functor respectively. The source is printed verbatim.
+ \item @{text "@{verbatim s}"} prints uninterpreted source text literally
+ as ASCII characters, using some type-writer font style.
+
\item @{text "@{file path}"} checks that @{text "path"} refers to a
file (or directory) and prints it verbatim.
--- a/src/Doc/antiquote_setup.ML Mon Oct 20 16:12:23 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Mon Oct 20 17:41:04 2014 +0200
@@ -33,15 +33,6 @@
| clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c);
-(* verbatim text *)
-
-val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
-
-val _ =
- Theory.setup (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
- (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")));
-
-
(* ML text *)
local
@@ -106,11 +97,7 @@
val kind' = if kind = "" then "ML" else "ML " ^ kind;
in
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
- (txt'
- |> (if Config.get ctxt Thy_Output.quotes then quote else I)
- |> (if Config.get ctxt Thy_Output.display
- then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
- else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
+ (Thy_Output.verbatim_text ctxt txt')
end);
in
@@ -281,13 +268,13 @@
entity_antiqs no_check "" @{binding case} #>
entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
- entity_antiqs no_check "isatt" @{binding setting} #>
- entity_antiqs check_system_option "isatt" @{binding system_option} #>
+ entity_antiqs no_check "isasystem" @{binding setting} #>
+ entity_antiqs check_system_option "isasystem" @{binding system_option} #>
entity_antiqs no_check "" @{binding inference} #>
- entity_antiqs no_check "isatt" @{binding executable} #>
+ entity_antiqs no_check "isasystem" @{binding executable} #>
entity_antiqs check_tool "isatool" @{binding tool} #>
entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
- entity_antiqs (K (is_action o #1)) "isatt" @{binding action});
+ entity_antiqs (K (is_action o #1)) "isasystem" @{binding action});
end;
--- a/src/Doc/isar.sty Mon Oct 20 16:12:23 2014 +0100
+++ b/src/Doc/isar.sty Mon Oct 20 17:41:04 2014 +0200
@@ -4,7 +4,7 @@
{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
\newcommand{\indexref}[3]{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)}}{\index{#3 (#1\ #2)}}}
-\newcommand{\isatt}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}}
+\newcommand{\isasystem}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}}
\newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt isabelle #1}}
\newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}}
--- a/src/HOL/Cardinals/document/root.tex Mon Oct 20 16:12:23 2014 +0100
+++ b/src/HOL/Cardinals/document/root.tex Mon Oct 20 17:41:04 2014 +0200
@@ -8,10 +8,8 @@
\urlstyle{rm}
\isabellestyle{it}
-% for uniform font size
-%\renewcommand{\isastyle}{\isastyleminor}
+\bibliographystyle{plain}
-\bibliographystyle{plain}
\begin{document}
\title{Ordinals and cardinals in HOL}
--- a/src/HOL/Library/Code_Test.thy Mon Oct 20 16:12:23 2014 +0100
+++ b/src/HOL/Library/Code_Test.thy Mon Oct 20 17:41:04 2014 +0200
@@ -131,10 +131,10 @@
"xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
"xml_of_term (Code_Evaluation.App t1 t2) = [xml.tagged (STR ''5'') None [xml.node (xml_of_term t1), xml.node (xml_of_term t2)]]"
"xml_of_term (Code_Evaluation.Abs x ty t) = [xml.tagged (STR ''4'') (Some x) [xml.node (xml_of_typ ty), xml.node (xml_of_term t)]]"
- (*
+ -- {*
FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent
uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.
- *)
+ *}
"xml_of_term (Code_Evaluation.Free x ty) = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
by(simp_all add: xml_of_term_def xml_tree_anything)
--- a/src/HOL/Parity.thy Mon Oct 20 16:12:23 2014 +0100
+++ b/src/HOL/Parity.thy Mon Oct 20 17:41:04 2014 +0200
@@ -431,7 +431,7 @@
"odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
-lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. zero_le_power_eq\<close>
+lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
"0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
proof (cases "even n")
case True
--- a/src/Pure/ML/exn_properties_polyml.ML Mon Oct 20 16:12:23 2014 +0100
+++ b/src/Pure/ML/exn_properties_polyml.ML Mon Oct 20 17:41:04 2014 +0200
@@ -19,7 +19,9 @@
fun props_of (loc: PolyML.location) =
(case YXML.parse_body (#file loc) of
[] => []
- | [XML.Text file] => [(Markup.fileN, file)]
+ | [XML.Text file] =>
+ if file = "Standard Basis" then []
+ else [(Markup.fileN, file)]
| body => XML.Decode.properties body);
fun position_of loc =
--- a/src/Pure/PIDE/resources.ML Mon Oct 20 16:12:23 2014 +0100
+++ b/src/Pure/PIDE/resources.ML Mon Oct 20 17:41:04 2014 +0200
@@ -222,8 +222,9 @@
val _ = check_path strict ctxt dir (name, pos);
in
space_explode "/" name
- |> map Thy_Output.verb_text
- |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
+ |> map Latex.output_ascii
+ |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
+ |> Thy_Output.enclose_isabelle_tt ctxt
end;
in
--- a/src/Pure/Thy/latex.ML Mon Oct 20 16:12:23 2014 +0100
+++ b/src/Pure/Thy/latex.ML Mon Oct 20 17:41:04 2014 +0200
@@ -6,6 +6,7 @@
signature LATEX =
sig
+ val output_ascii: string -> string
val output_known_symbols: (string -> bool) * (string -> bool) ->
Symbol.symbol list -> string
val output_symbols: Symbol.symbol list -> string
@@ -30,6 +31,18 @@
structure Latex: LATEX =
struct
+(* literal ASCII *)
+
+val output_ascii =
+ translate_string
+ (fn " " => "\\ "
+ | "\t" => "\\ "
+ | "\n" => "\\isanewline\n"
+ | s =>
+ if exists_string (fn s' => s = s') "#$%^&_{}~\\"
+ then enclose "{\\char`\\" "}" s else s);
+
+
(* symbol output *)
local
--- a/src/Pure/Thy/thy_output.ML Mon Oct 20 16:12:23 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Mon Oct 20 17:41:04 2014 +0200
@@ -34,7 +34,8 @@
val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
Token.src -> 'a list -> Pretty.T list
val output: Proof.context -> Pretty.T list -> string
- val verb_text: string -> string
+ val verbatim_text: Proof.context -> string -> string
+ val enclose_isabelle_tt: Proof.context -> string -> string
end;
structure Thy_Output: THY_OUTPUT =
@@ -469,6 +470,10 @@
fun tweak_line ctxt s =
if Config.get ctxt display then s else Symbol.strip_blanks s;
+fun tweak_lines ctxt s =
+ if Config.get ctxt display then s
+ else s |> split_lines |> map Symbol.strip_blanks |> space_implode " ";
+
fun pretty_text ctxt =
Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
@@ -542,15 +547,15 @@
fun output ctxt prts =
prts
- |> (if Config.get ctxt quotes then map Pretty.quote else I)
+ |> Config.get ctxt quotes ? map Pretty.quote
|> (if Config.get ctxt display then
- map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
- #> space_implode "\\isasep\\isanewline%\n"
- #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
- else
- map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
- #> space_implode "\\isasep\\isanewline%\n"
- #> enclose "\\isa{" "}");
+ map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
+ #> space_implode "\\isasep\\isanewline%\n"
+ #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ else
+ map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
+ #> space_implode "\\isasep\\isanewline%\n"
+ #> enclose "\\isa{" "}");
@@ -636,23 +641,31 @@
in output ctxt (maybe_pretty_source pretty_term ctxt prop_src [prop]) end));
-(* ML text *)
+(* verbatim text *)
+
+fun enclose_isabelle_tt ctxt =
+ if Config.get ctxt display
+ then enclose "\\begin{isabellett}%\n" "%\n\\end{isabellett}"
+ else enclose "\\isatt{" "}";
-val verb_text =
- split_lines
- #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
- #> space_implode "\\isasep\\isanewline%\n";
+fun verbatim_text ctxt =
+ tweak_lines ctxt
+ #> Latex.output_ascii
+ #> enclose_isabelle_tt ctxt;
+
+val _ = Theory.setup
+ (antiquotation @{binding verbatim} (Scan.lift Args.text) (verbatim_text o #context));
+
+
+(* ML text *)
local
fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
- (fn {context, ...} => fn source =>
- (ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) (ml source);
- Symbol_Pos.source_content source
- |> #1
- |> (if Config.get context quotes then quote else I)
- |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
- else verb_text)));
+ (fn {context = ctxt, ...} => fn source =>
+ (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source) (ml source);
+ Symbol_Pos.source_content source |> #1
+ |> verbatim_text ctxt));
fun ml_enclose bg en source =
ML_Lex.read Position.none bg @