official support for "tt" style variants, avoid fragile \verb in LaTeX;
authorwenzelm
Mon Oct 20 16:52:36 2014 +0200 (2014-10-20)
changeset 5871623a380cc45f4
parent 58715 cb8d2470623b
child 58717 500863881874
official support for "tt" style variants, avoid fragile \verb in LaTeX;
official document antiquotation @{verbatim};
NEWS
lib/texinputs/isabelle.sty
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/antiquote_setup.ML
src/Doc/isar.sty
src/Pure/PIDE/resources.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Mon Oct 20 14:11:14 2014 +0200
     1.2 +++ b/NEWS	Mon Oct 20 16:52:36 2014 +0200
     1.3 @@ -146,6 +146,17 @@
     1.4  argument. Minor INCOMPATIBILITY.
     1.5  
     1.6  
     1.7 +*** Document preparation ***
     1.8 +
     1.9 +* Official support for "tt" style variants, via \isatt{...} or
    1.10 +\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
    1.11 +verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
    1.12 +as argument to other macros (such as footnotes).
    1.13 +
    1.14 +* Document antiquotation @{verbatim} prints ASCII text literally in "tt"
    1.15 +style.
    1.16 +
    1.17 +
    1.18  *** ML ***
    1.19  
    1.20  * Tactical PARALLEL_ALLGOALS is the most common way to refer to
     2.1 --- a/lib/texinputs/isabelle.sty	Mon Oct 20 14:11:14 2014 +0200
     2.2 +++ b/lib/texinputs/isabelle.sty	Mon Oct 20 16:52:36 2014 +0200
     2.3 @@ -9,7 +9,9 @@
     2.4  \newcommand{\isabellecontext}{UNKNOWN}
     2.5  
     2.6  \newcommand{\isastyle}{\UNDEF}
     2.7 +\newcommand{\isastylett}{\UNDEF}
     2.8  \newcommand{\isastyleminor}{\UNDEF}
     2.9 +\newcommand{\isastyleminortt}{\UNDEF}
    2.10  \newcommand{\isastylescript}{\UNDEF}
    2.11  \newcommand{\isastyletext}{\normalsize\rm}
    2.12  \newcommand{\isastyletxt}{\rm}
    2.13 @@ -46,11 +48,22 @@
    2.14  \isa@parskip\parskip\parskip0pt%
    2.15  \isaspacing\isastyle}{\par}
    2.16  
    2.17 +\newenvironment{isabellebodytt}{%
    2.18 +\isamarkuptrue\par%
    2.19 +\isa@parindent\parindent\parindent0pt%
    2.20 +\isa@parskip\parskip\parskip0pt%
    2.21 +\isaspacing\isastylett}{\par}
    2.22 +
    2.23  \newenvironment{isabelle}
    2.24  {\begin{trivlist}\begin{isabellebody}\item\relax}
    2.25  {\end{isabellebody}\end{trivlist}}
    2.26  
    2.27 +\newenvironment{isabellett}
    2.28 +{\begin{trivlist}\begin{isabellebodytt}\item\relax}
    2.29 +{\end{isabellebodytt}\end{trivlist}}
    2.30 +
    2.31  \newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
    2.32 +\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
    2.33  
    2.34  \newcommand{\isaindent}[1]{\hphantom{#1}}
    2.35  \newcommand{\isanewline}{\mbox{}\par\mbox{}}
    2.36 @@ -133,7 +146,9 @@
    2.37  
    2.38  \newcommand{\isabellestyledefault}{%
    2.39  \def\isastyle{\small\tt\slshape}%
    2.40 +\def\isastylett{\small\tt}%
    2.41  \def\isastyleminor{\small\tt\slshape}%
    2.42 +\def\isastyleminortt{\small\tt}%
    2.43  \def\isastylescript{\footnotesize\tt\slshape}%
    2.44  \isachardefaults%
    2.45  }
    2.46 @@ -141,14 +156,18 @@
    2.47  
    2.48  \newcommand{\isabellestylett}{%
    2.49  \def\isastyle{\small\tt}%
    2.50 +\def\isastylett{\small\tt}%
    2.51  \def\isastyleminor{\small\tt}%
    2.52 +\def\isastyleminortt{\small\tt}%
    2.53  \def\isastylescript{\footnotesize\tt}%
    2.54  \isachardefaults%
    2.55  }
    2.56  
    2.57  \newcommand{\isabellestyleit}{%
    2.58  \def\isastyle{\small\it}%
    2.59 +\def\isastylett{\small\tt}%
    2.60  \def\isastyleminor{\it}%
    2.61 +\def\isastyleminortt{\tt}%
    2.62  \def\isastylescript{\footnotesize\it}%
    2.63  \isachardefaults%
    2.64  \def\isacharunderscorekeyword{\mbox{-}}%
    2.65 @@ -206,7 +225,9 @@
    2.66  \newcommand{\isabellestylesl}{%
    2.67  \isabellestyleit%
    2.68  \def\isastyle{\small\sl}%
    2.69 +\def\isastylett{\small\tt}%
    2.70  \def\isastyleminor{\sl}%
    2.71 +\def\isastyleminortt{\tt}%
    2.72  \def\isastylescript{\footnotesize\sl}%
    2.73  }
    2.74  
     3.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Oct 20 14:11:14 2014 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Oct 20 16:52:36 2014 +0200
     3.3 @@ -125,6 +125,7 @@
     3.4      @{antiquotation_def ML_type} & : & @{text antiquotation} \\
     3.5      @{antiquotation_def ML_structure} & : & @{text antiquotation} \\
     3.6      @{antiquotation_def ML_functor} & : & @{text antiquotation} \\
     3.7 +    @{antiquotation_def verbatim} & : & @{text antiquotation} \\
     3.8      @{antiquotation_def "file"} & : & @{text antiquotation} \\
     3.9      @{antiquotation_def "url"} & : & @{text antiquotation} \\
    3.10      @{antiquotation_def "cite"} & : & @{text antiquotation} \\
    3.11 @@ -179,6 +180,7 @@
    3.12        @@{antiquotation ML_type} options @{syntax text} |
    3.13        @@{antiquotation ML_structure} options @{syntax text} |
    3.14        @@{antiquotation ML_functor} options @{syntax text} |
    3.15 +      @@{antiquotation verbatim} options @{syntax text} |
    3.16        @@{antiquotation "file"} options @{syntax name} |
    3.17        @@{antiquotation file_unchecked} options @{syntax name} |
    3.18        @@{antiquotation url} options @{syntax name} |
    3.19 @@ -271,6 +273,9 @@
    3.20    check text @{text s} as ML value, infix operator, type, structure,
    3.21    and functor respectively.  The source is printed verbatim.
    3.22  
    3.23 +  \item @{text "@{verbatim s}"} prints uninterpreted source text literally
    3.24 +  as ASCII characters, using some type-writer font style.
    3.25 +
    3.26    \item @{text "@{file path}"} checks that @{text "path"} refers to a
    3.27    file (or directory) and prints it verbatim.
    3.28  
     4.1 --- a/src/Doc/antiquote_setup.ML	Mon Oct 20 14:11:14 2014 +0200
     4.2 +++ b/src/Doc/antiquote_setup.ML	Mon Oct 20 16:52:36 2014 +0200
     4.3 @@ -33,15 +33,6 @@
     4.4    | clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c);
     4.5  
     4.6  
     4.7 -(* verbatim text *)
     4.8 -
     4.9 -val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
    4.10 -
    4.11 -val _ =
    4.12 -  Theory.setup (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
    4.13 -    (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")));
    4.14 -
    4.15 -
    4.16  (* ML text *)
    4.17  
    4.18  local
    4.19 @@ -106,11 +97,7 @@
    4.20        val kind' = if kind = "" then "ML" else "ML " ^ kind;
    4.21      in
    4.22        "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
    4.23 -      (txt'
    4.24 -      |> (if Config.get ctxt Thy_Output.quotes then quote else I)
    4.25 -      |> (if Config.get ctxt Thy_Output.display
    4.26 -          then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    4.27 -          else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    4.28 +      (Thy_Output.verbatim_text ctxt txt')
    4.29      end);
    4.30  
    4.31  in
    4.32 @@ -281,13 +268,13 @@
    4.33      entity_antiqs no_check "" @{binding case} #>
    4.34      entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
    4.35      entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
    4.36 -    entity_antiqs no_check "isatt" @{binding setting} #>
    4.37 -    entity_antiqs check_system_option "isatt" @{binding system_option} #>
    4.38 +    entity_antiqs no_check "isasystem" @{binding setting} #>
    4.39 +    entity_antiqs check_system_option "isasystem" @{binding system_option} #>
    4.40      entity_antiqs no_check "" @{binding inference} #>
    4.41 -    entity_antiqs no_check "isatt" @{binding executable} #>
    4.42 +    entity_antiqs no_check "isasystem" @{binding executable} #>
    4.43      entity_antiqs check_tool "isatool" @{binding tool} #>
    4.44      entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
    4.45 -    entity_antiqs (K (is_action o #1)) "isatt" @{binding action});
    4.46 +    entity_antiqs (K (is_action o #1)) "isasystem" @{binding action});
    4.47  
    4.48  end;
    4.49  
     5.1 --- a/src/Doc/isar.sty	Mon Oct 20 14:11:14 2014 +0200
     5.2 +++ b/src/Doc/isar.sty	Mon Oct 20 16:52:36 2014 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4  {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
     5.5  \newcommand{\indexref}[3]{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)}}{\index{#3 (#1\ #2)}}}
     5.6  
     5.7 -\newcommand{\isatt}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}}
     5.8 +\newcommand{\isasystem}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}}
     5.9  \newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt isabelle #1}}
    5.10  
    5.11  \newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}}
     6.1 --- a/src/Pure/PIDE/resources.ML	Mon Oct 20 14:11:14 2014 +0200
     6.2 +++ b/src/Pure/PIDE/resources.ML	Mon Oct 20 16:52:36 2014 +0200
     6.3 @@ -222,8 +222,9 @@
     6.4      val _ = check_path strict ctxt dir (name, pos);
     6.5    in
     6.6      space_explode "/" name
     6.7 -    |> map Thy_Output.verb_text
     6.8 -    |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
     6.9 +    |> map Latex.output_ascii
    6.10 +    |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
    6.11 +    |> Thy_Output.enclose_isabelle_tt ctxt
    6.12    end;
    6.13  
    6.14  in
     7.1 --- a/src/Pure/Thy/latex.ML	Mon Oct 20 14:11:14 2014 +0200
     7.2 +++ b/src/Pure/Thy/latex.ML	Mon Oct 20 16:52:36 2014 +0200
     7.3 @@ -6,6 +6,7 @@
     7.4  
     7.5  signature LATEX =
     7.6  sig
     7.7 +  val output_ascii: string -> string
     7.8    val output_known_symbols: (string -> bool) * (string -> bool) ->
     7.9      Symbol.symbol list -> string
    7.10    val output_symbols: Symbol.symbol list -> string
    7.11 @@ -30,6 +31,18 @@
    7.12  structure Latex: LATEX =
    7.13  struct
    7.14  
    7.15 +(* literal ASCII *)
    7.16 +
    7.17 +val output_ascii =
    7.18 +  translate_string
    7.19 +    (fn " " => "\\ "
    7.20 +      | "\t" => "\\ "
    7.21 +      | "\n" => "\\isanewline\n"
    7.22 +      | s =>
    7.23 +          if exists_string (fn s' => s = s') "#$%^&_{}~\\"
    7.24 +          then enclose "{\\char`\\" "}" s else s);
    7.25 +
    7.26 +
    7.27  (* symbol output *)
    7.28  
    7.29  local
     8.1 --- a/src/Pure/Thy/thy_output.ML	Mon Oct 20 14:11:14 2014 +0200
     8.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Oct 20 16:52:36 2014 +0200
     8.3 @@ -34,7 +34,8 @@
     8.4    val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
     8.5      Token.src -> 'a list -> Pretty.T list
     8.6    val output: Proof.context -> Pretty.T list -> string
     8.7 -  val verb_text: string -> string
     8.8 +  val verbatim_text: Proof.context -> string -> string
     8.9 +  val enclose_isabelle_tt: Proof.context -> string -> string
    8.10  end;
    8.11  
    8.12  structure Thy_Output: THY_OUTPUT =
    8.13 @@ -469,6 +470,10 @@
    8.14  fun tweak_line ctxt s =
    8.15    if Config.get ctxt display then s else Symbol.strip_blanks s;
    8.16  
    8.17 +fun tweak_lines ctxt s =
    8.18 +  if Config.get ctxt display then s
    8.19 +  else s |> split_lines |> map Symbol.strip_blanks |> space_implode " ";
    8.20 +
    8.21  fun pretty_text ctxt =
    8.22    Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
    8.23  
    8.24 @@ -542,15 +547,15 @@
    8.25  
    8.26  fun output ctxt prts =
    8.27    prts
    8.28 -  |> (if Config.get ctxt quotes then map Pretty.quote else I)
    8.29 +  |> Config.get ctxt quotes ? map Pretty.quote
    8.30    |> (if Config.get ctxt display then
    8.31 -    map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
    8.32 -    #> space_implode "\\isasep\\isanewline%\n"
    8.33 -    #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    8.34 -  else
    8.35 -    map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
    8.36 -    #> space_implode "\\isasep\\isanewline%\n"
    8.37 -    #> enclose "\\isa{" "}");
    8.38 +        map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
    8.39 +        #> space_implode "\\isasep\\isanewline%\n"
    8.40 +        #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    8.41 +      else
    8.42 +        map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
    8.43 +        #> space_implode "\\isasep\\isanewline%\n"
    8.44 +        #> enclose "\\isa{" "}");
    8.45  
    8.46  
    8.47  
    8.48 @@ -636,23 +641,31 @@
    8.49        in output ctxt (maybe_pretty_source pretty_term ctxt prop_src [prop]) end));
    8.50  
    8.51  
    8.52 -(* ML text *)
    8.53 +(* verbatim text *)
    8.54 +
    8.55 +fun enclose_isabelle_tt ctxt =
    8.56 +  if Config.get ctxt display
    8.57 +  then enclose "\\begin{isabellett}%\n" "%\n\\end{isabellett}"
    8.58 +  else enclose "\\isatt{" "}";
    8.59  
    8.60 -val verb_text =
    8.61 -  split_lines
    8.62 -  #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
    8.63 -  #> space_implode "\\isasep\\isanewline%\n";
    8.64 +fun verbatim_text ctxt =
    8.65 +  tweak_lines ctxt
    8.66 +  #> Latex.output_ascii
    8.67 +  #> enclose_isabelle_tt ctxt;
    8.68 +
    8.69 +val _ = Theory.setup
    8.70 +  (antiquotation @{binding verbatim} (Scan.lift Args.text) (verbatim_text o #context));
    8.71 +
    8.72 +
    8.73 +(* ML text *)
    8.74  
    8.75  local
    8.76  
    8.77  fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
    8.78 -  (fn {context, ...} => fn source =>
    8.79 -   (ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) (ml source);
    8.80 -    Symbol_Pos.source_content source
    8.81 -    |> #1
    8.82 -    |> (if Config.get context quotes then quote else I)
    8.83 -    |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    8.84 -        else verb_text)));
    8.85 +  (fn {context = ctxt, ...} => fn source =>
    8.86 +   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source) (ml source);
    8.87 +    Symbol_Pos.source_content source |> #1
    8.88 +    |> verbatim_text ctxt));
    8.89  
    8.90  fun ml_enclose bg en source =
    8.91    ML_Lex.read Position.none bg @