# HG changeset patch # User wenzelm # Date 1413819664 -7200 # Node ID e4f4925d4a9dccc716bc2cf804a1af58a26f20c1 # Parent 572a5a870c84fddb501410a4500e4d1c3f9d1348# Parent ac4f764c5be141bab14fe7ebbfc71165ff63baf4 merged diff -r 572a5a870c84 -r e4f4925d4a9d NEWS --- 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 diff -r 572a5a870c84 -r e4f4925d4a9d lib/texinputs/isabelle.sty --- 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}% } diff -r 572a5a870c84 -r e4f4925d4a9d src/Doc/Isar_Ref/Document_Preparation.thy --- 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. diff -r 572a5a870c84 -r e4f4925d4a9d src/Doc/antiquote_setup.ML --- 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 "_" => "-" | "\" => "-" | 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; diff -r 572a5a870c84 -r e4f4925d4a9d src/Doc/isar.sty --- 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}} diff -r 572a5a870c84 -r e4f4925d4a9d src/HOL/Cardinals/document/root.tex --- 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} diff -r 572a5a870c84 -r e4f4925d4a9d src/HOL/Library/Code_Test.thy --- 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) diff -r 572a5a870c84 -r e4f4925d4a9d src/HOL/Parity.thy --- 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 \ 0 \ a ^ n \ 0 \ a" by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) -lemma zero_le_power_iff [presburger]: -- \FIXME cf. zero_le_power_eq\ +lemma zero_le_power_iff [presburger]: -- \FIXME cf. @{text zero_le_power_eq}\ "0 \ a ^ n \ 0 \ a \ even n" proof (cases "even n") case True diff -r 572a5a870c84 -r e4f4925d4a9d src/Pure/ML/exn_properties_polyml.ML --- 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 = diff -r 572a5a870c84 -r e4f4925d4a9d src/Pure/PIDE/resources.ML --- 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 diff -r 572a5a870c84 -r e4f4925d4a9d src/Pure/Thy/latex.ML --- 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 diff -r 572a5a870c84 -r e4f4925d4a9d src/Pure/Thy/thy_output.ML --- 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 @