clarified control antiquotations: decode control symbol to get name;
authorwenzelm
Sun Oct 18 20:28:29 2015 +0200 (2015-10-18)
changeset 6147334d1913f0b20
parent 61472 6458760261ca
child 61474 6cc07122ca14
clarified control antiquotations: decode control symbol to get name;
document antiquotations @{emph}, @{bold};
symbol interpretation for \<^emph>;
tuned;
NEWS
etc/symbols
lib/texinputs/isabelle.sty
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/Isar_Ref/Outer_Syntax.thy
src/Pure/General/antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/rail.ML
     1.1 --- a/NEWS	Sun Oct 18 18:09:48 2015 +0200
     1.2 +++ b/NEWS	Sun Oct 18 20:28:29 2015 +0200
     1.3 @@ -22,8 +22,8 @@
     1.4  * Toplevel theorem statement 'proposition' is another alias for
     1.5  'theorem'.
     1.6  
     1.7 -* There is a new short form of antiquotations: \<^foo>\<open>...\<close> is
     1.8 -equivalent to @{"\<^foo>" \<open>...\<close>} for control symbols.
     1.9 +* There is a new short form for antiquotations with a single argument
    1.10 +that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>}.
    1.11  
    1.12  
    1.13  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.14 @@ -82,6 +82,10 @@
    1.15  'text' (with antiquotations and control symbols). The key difference is
    1.16  the lack of the surrounding isabelle markup environment in output.
    1.17  
    1.18 +* Document antiquotations @{emph} and @{bold} output LaTeX source
    1.19 +recursively, adding appropriate text style markup. These are typically
    1.20 +used in the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.
    1.21 +
    1.22  
    1.23  *** Isar ***
    1.24  
     2.1 --- a/etc/symbols	Sun Oct 18 18:09:48 2015 +0200
     2.2 +++ b/etc/symbols	Sun Oct 18 20:28:29 2015 +0200
     2.3 @@ -359,7 +359,7 @@
     2.4  \<^item>                code: 0x0025aa  group: control  font: IsabelleText
     2.5  \<^enum>                code: 0x0025b8  group: control  font: IsabelleText
     2.6  \<^descr>               code: 0x0027a7  group: control  font: IsabelleText
     2.7 -#\<^emph>                code: 0x002217  group: control  font: IsabelleText
     2.8 +\<^emph>                code: 0x002217  group: control  font: IsabelleText
     2.9  \<^bold>                code: 0x002759  group: control  font: IsabelleText
    2.10  \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
    2.11  \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
     3.1 --- a/lib/texinputs/isabelle.sty	Sun Oct 18 18:09:48 2015 +0200
     3.2 +++ b/lib/texinputs/isabelle.sty	Sun Oct 18 20:28:29 2015 +0200
     3.3 @@ -44,6 +44,7 @@
     3.4  \def\isactrlmedskip{\medskip}
     3.5  \def\isactrlbigskip{\bigskip}
     3.6  
     3.7 +\newcommand{\isaantiqcontrol}[1]{\isatt{{\char`\\}{\char`\<}{\char`\^}#1{\char`\>}}}
     3.8  \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
     3.9  
    3.10  \newdimen\isa@parindent\newdimen\isa@parskip
     4.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Oct 18 18:09:48 2015 +0200
     4.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Oct 18 20:28:29 2015 +0200
     4.3 @@ -81,7 +81,6 @@
     4.4  
     4.5  text \<open>
     4.6    \begin{matharray}{rcl}
     4.7 -    @{command_def "print_antiquotations"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
     4.8      @{antiquotation_def "theory"} & : & @{text antiquotation} \\
     4.9      @{antiquotation_def "thm"} & : & @{text antiquotation} \\
    4.10      @{antiquotation_def "lemma"} & : & @{text antiquotation} \\
    4.11 @@ -104,10 +103,13 @@
    4.12      @{antiquotation_def ML_type} & : & @{text antiquotation} \\
    4.13      @{antiquotation_def ML_structure} & : & @{text antiquotation} \\
    4.14      @{antiquotation_def ML_functor} & : & @{text antiquotation} \\
    4.15 +    @{antiquotation_def emph} & : & @{text antiquotation} \\
    4.16 +    @{antiquotation_def bold} & : & @{text antiquotation} \\
    4.17      @{antiquotation_def verbatim} & : & @{text antiquotation} \\
    4.18      @{antiquotation_def "file"} & : & @{text antiquotation} \\
    4.19      @{antiquotation_def "url"} & : & @{text antiquotation} \\
    4.20      @{antiquotation_def "cite"} & : & @{text antiquotation} \\
    4.21 +    @{command_def "print_antiquotations"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
    4.22    \end{matharray}
    4.23  
    4.24    The overall content of an Isabelle/Isar theory may alternate between
    4.25 @@ -132,16 +134,14 @@
    4.26    \<^medskip>
    4.27    Antiquotations are in general written @{verbatim "@{"}@{text "name
    4.28    [options] arguments"}@{verbatim "}"}. The short form @{verbatim
    4.29 -  "\<^control>"}@{text "\<open>argument\<close>"} (without surrounding @{verbatim
    4.30 -  "@{"}@{text "\<dots>"}@{verbatim "}"}) works where the name is a single control
    4.31 -  symbol and the argument a single cartouche.
    4.32 +  "\<^name>"}@{text "\<open>argument\<close>"} (without surrounding @{verbatim
    4.33 +  "@{"}@{text "\<dots>"}@{verbatim "}"}) works for a single argument that is a
    4.34 +  cartouche.
    4.35  
    4.36    @{rail \<open>
    4.37 -    @@{command print_antiquotations} ('!'?)
    4.38 -    ;
    4.39      @{syntax_def antiquotation}:
    4.40 -      '@{' antiquotation_body '}' |
    4.41 -      @{syntax_ref control_symbol} @{syntax_ref cartouche}
    4.42 +      '@' '{' antiquotation_body '}' |
    4.43 +      '\\' '<' '^' @{syntax_ref name} '>' @{syntax_ref cartouche}
    4.44    \<close>}
    4.45  
    4.46    %% FIXME less monolithic presentation, move to individual sections!?
    4.47 @@ -172,6 +172,8 @@
    4.48        @@{antiquotation ML_type} options @{syntax text} |
    4.49        @@{antiquotation ML_structure} options @{syntax text} |
    4.50        @@{antiquotation ML_functor} options @{syntax text} |
    4.51 +      @@{antiquotation emph} options @{syntax text} |
    4.52 +      @@{antiquotation bold} options @{syntax text} |
    4.53        @@{antiquotation verbatim} options @{syntax text} |
    4.54        @@{antiquotation "file"} options @{syntax name} |
    4.55        @@{antiquotation file_unchecked} options @{syntax name} |
    4.56 @@ -185,16 +187,14 @@
    4.57      styles: '(' (style + ',') ')'
    4.58      ;
    4.59      style: (@{syntax name} +)
    4.60 +    ;
    4.61 +    @@{command print_antiquotations} ('!'?)
    4.62    \<close>}
    4.63  
    4.64    Note that the syntax of antiquotations may \emph{not} include source
    4.65    comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
    4.66    text @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"}.
    4.67  
    4.68 -  \<^descr> @{command "print_antiquotations"} prints all document antiquotations
    4.69 -  that are defined in the current context; the ``@{text "!"}'' option
    4.70 -  indicates extra verbosity.
    4.71 -
    4.72    \<^descr> @{text "@{theory A}"} prints the name @{text "A"}, which is
    4.73    guaranteed to refer to a valid ancestor theory in the current
    4.74    context.
    4.75 @@ -266,6 +266,12 @@
    4.76    check text @{text s} as ML value, infix operator, type, structure,
    4.77    and functor respectively.  The source is printed verbatim.
    4.78  
    4.79 +  \<^descr> @{text "@{emph s}"} prints document source recursively, with {\LaTeX}
    4.80 +  markup @{verbatim \<open>\emph{\<close>}@{text "\<dots>"}@{verbatim \<open>}\<close>}.
    4.81 +
    4.82 +  \<^descr> @{text "@{bold s}"} prints document source recursively, with {\LaTeX}
    4.83 +  markup @{verbatim \<open>\textbf{\<close>}@{text "\<dots>"}@{verbatim \<open>}\<close>}.
    4.84 +
    4.85    \<^descr> @{text "@{verbatim s}"} prints uninterpreted source text literally
    4.86    as ASCII characters, using some type-writer font style.
    4.87  
    4.88 @@ -292,6 +298,10 @@
    4.89    @{antiquotation_option_def cite_macro}, or the configuration option
    4.90    @{attribute cite_macro} in the context. For example, @{text "@{cite
    4.91    [cite_macro = nocite] foobar}"} produces @{verbatim \<open>\nocite{foobar}\<close>}.
    4.92 +
    4.93 +  \<^descr> @{command "print_antiquotations"} prints all document antiquotations
    4.94 +  that are defined in the current context; the ``@{text "!"}'' option
    4.95 +  indicates extra verbosity.
    4.96  \<close>
    4.97  
    4.98  
     5.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Sun Oct 18 18:09:48 2015 +0200
     5.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Sun Oct 18 20:28:29 2015 +0200
     5.3 @@ -114,7 +114,6 @@
     5.4      @{syntax_def cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
     5.5      @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*}"} \\[1ex]
     5.6  
     5.7 -    @{text control_symbol} & = & @{verbatim \<open>\\<close>}@{verbatim "<^"}@{text ident}@{verbatim ">"} \\
     5.8      @{text letter} & = & @{text "latin  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
     5.9      @{text subscript} & = & @{verbatim "\<^sub>"} \\
    5.10      @{text quasiletter} & = & @{text "letter  |  digit  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "'"} \\
     6.1 --- a/src/Pure/General/antiquote.ML	Sun Oct 18 18:09:48 2015 +0200
     6.2 +++ b/src/Pure/General/antiquote.ML	Sun Oct 18 20:28:29 2015 +0200
     6.3 @@ -6,14 +6,14 @@
     6.4  
     6.5  signature ANTIQUOTE =
     6.6  sig
     6.7 -  type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
     6.8 -  datatype 'a antiquote =
     6.9 -    Text of 'a | Control of Symbol_Pos.T * Symbol_Pos.T list | Antiq of antiq
    6.10 +  type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}
    6.11 +  type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
    6.12 +  datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
    6.13    type text_antiquote = Symbol_Pos.T list antiquote
    6.14    val range: text_antiquote list -> Position.range
    6.15    val split_lines: text_antiquote list -> text_antiquote list list
    6.16    val antiq_reports: 'a antiquote list -> Position.report list
    6.17 -  val scan_control: Symbol_Pos.T list -> (Symbol_Pos.T * Symbol_Pos.T list) * Symbol_Pos.T list
    6.18 +  val scan_control: Symbol_Pos.T list -> control * Symbol_Pos.T list
    6.19    val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
    6.20    val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
    6.21    val read': Position.T -> Symbol_Pos.T list -> text_antiquote list
    6.22 @@ -25,15 +25,15 @@
    6.23  
    6.24  (* datatype antiquote *)
    6.25  
    6.26 -type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range};
    6.27 -datatype 'a antiquote =
    6.28 -  Text of 'a | Control of Symbol_Pos.T * Symbol_Pos.T list | Antiq of antiq;
    6.29 +type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list};
    6.30 +type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list};
    6.31 +datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq;
    6.32  
    6.33  type text_antiquote = Symbol_Pos.T list antiquote;
    6.34  
    6.35  fun antiquote_range (Text ss) = Symbol_Pos.range ss
    6.36 -  | antiquote_range (Control (s, ss)) = Symbol_Pos.range (s :: ss)
    6.37 -  | antiquote_range (Antiq (_, {range, ...})) = range;
    6.38 +  | antiquote_range (Control {range, ...}) = range
    6.39 +  | antiquote_range (Antiq {range, ...}) = range;
    6.40  
    6.41  fun range ants =
    6.42    if null ants then Position.no_range
    6.43 @@ -60,8 +60,8 @@
    6.44  
    6.45  fun antiq_reports ants = ants |> maps
    6.46    (fn Text _ => []
    6.47 -    | Control (s, ss) => [(#1 (Symbol_Pos.range (s :: ss)), Markup.antiquoted)]
    6.48 -    | Antiq (_, {start, stop, range = (pos, _)}) =>
    6.49 +    | Control {range = (pos, _), ...} => [(pos, Markup.antiquoted)]
    6.50 +    | Antiq {start, stop, range = (pos, _), ...} =>
    6.51          [(start, Markup.antiquote),
    6.52           (stop, Markup.antiquote),
    6.53           (pos, Markup.antiquoted),
    6.54 @@ -91,17 +91,22 @@
    6.55  
    6.56  val scan_control =
    6.57    Scan.one (Symbol.is_control o Symbol_Pos.symbol) --
    6.58 -  (Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2);
    6.59 +  Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >>
    6.60 +    (fn ((control, pos), (_, body)) =>
    6.61 +      let
    6.62 +        val Symbol.Ctrl name = Symbol.decode control;
    6.63 +        val range = Symbol_Pos.range ((control, pos) :: body);
    6.64 +      in {name = (name, pos), range = range, body = body} end);
    6.65  
    6.66  val scan_antiq =
    6.67    Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
    6.68      Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
    6.69 -      (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos)))
    6.70 -  >> (fn (pos1, (pos2, ((body, pos3), pos4))) =>
    6.71 -      (flat body,
    6.72 -        {start = Position.set_range (pos1, pos2),
    6.73 -         stop = Position.set_range (pos3, pos4),
    6.74 -         range = Position.range pos1 pos4}));
    6.75 +      (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
    6.76 +    (fn (pos1, (pos2, ((body, pos3), pos4))) =>
    6.77 +      {start = Position.set_range (pos1, pos2),
    6.78 +       stop = Position.set_range (pos3, pos4),
    6.79 +       range = Position.range pos1 pos4,
    6.80 +       body = flat body});
    6.81  
    6.82  val scan_antiquote =
    6.83    scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text;
     7.1 --- a/src/Pure/ML/ml_context.ML	Sun Oct 18 18:09:48 2015 +0200
     7.2 +++ b/src/Pure/ML/ml_context.ML	Sun Oct 18 20:28:29 2015 +0200
     7.3 @@ -169,12 +169,11 @@
     7.4                            ML_Syntax.atomic (ML_Syntax.print_range range)) ctxt;
     7.5                    in (decl #> tokenize range, ctxt') end
     7.6                  else (K ([], [tok]), ctxt)
     7.7 -            | expand (Antiquote.Control (s, ss)) ctxt =
     7.8 -                let val range = Symbol_Pos.range (s :: ss)
     7.9 -                in expand_src range (Token.src s [Token.read_cartouche ss]) ctxt end
    7.10 -            | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
    7.11 -                let val keywords = Thy_Header.get_keywords' ctxt
    7.12 -                in expand_src range (Token.read_antiq keywords antiq (ss, #1 range)) ctxt end;
    7.13 +            | expand (Antiquote.Control {name, range, body}) ctxt =
    7.14 +                expand_src range (Token.src name [Token.read_cartouche body]) ctxt
    7.15 +            | expand (Antiquote.Antiq {range, body, ...}) ctxt =
    7.16 +                expand_src range
    7.17 +                  (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt;
    7.18  
    7.19            val ctxt =
    7.20              (case opt_ctxt of
     8.1 --- a/src/Pure/Thy/latex.ML	Sun Oct 18 18:09:48 2015 +0200
     8.2 +++ b/src/Pure/Thy/latex.ML	Sun Oct 18 20:28:29 2015 +0200
     8.3 @@ -112,10 +112,12 @@
     8.4  
     8.5  val output_syms_antiq =
     8.6    (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
     8.7 -    | Antiquote.Control (s, ss) => output_symbols (map Symbol_Pos.symbol (s :: ss))
     8.8 -    | Antiquote.Antiq (ss, _) =>
     8.9 +    | Antiquote.Control {name = (name, _), body, ...} =>
    8.10 +        "\\isaantiqcontrol{" ^ output_symbols (Symbol.explode name) ^ "}" ^
    8.11 +        output_symbols (map Symbol_Pos.symbol body)
    8.12 +    | Antiquote.Antiq {body, ...} =>
    8.13          enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
    8.14 -          (output_symbols (map Symbol_Pos.symbol ss)));
    8.15 +          (output_symbols (map Symbol_Pos.symbol body)));
    8.16  
    8.17  val output_ctrl_symbols = implode o map output_ctrl_sym;
    8.18  
     9.1 --- a/src/Pure/Thy/thy_output.ML	Sun Oct 18 18:09:48 2015 +0200
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Oct 18 20:28:29 2015 +0200
     9.3 @@ -176,9 +176,9 @@
     9.4  in
     9.5  
     9.6  fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
     9.7 -  | eval_antiquote state (Antiquote.Control (control, arg)) =
     9.8 -      eval_antiq state ([], Token.src control [Token.read_cartouche arg])
     9.9 -  | eval_antiquote state (Antiquote.Antiq (ss, {range = (pos, _), ...})) =
    9.10 +  | eval_antiquote state (Antiquote.Control {name, body, ...}) =
    9.11 +      eval_antiq state ([], Token.src name [Token.read_cartouche body])
    9.12 +  | eval_antiquote state (Antiquote.Antiq {range = (pos, _), body, ...}) =
    9.13        let
    9.14          val keywords =
    9.15            (case try Toplevel.presentation_context_of state of
    9.16 @@ -186,7 +186,7 @@
    9.17            | NONE =>
    9.18                error ("Unknown context -- cannot expand document antiquotations" ^
    9.19                  Position.here pos));
    9.20 -      in eval_antiq state (Token.read_antiq keywords antiq (ss, pos)) end;
    9.21 +      in eval_antiq state (Token.read_antiq keywords antiq (body, pos)) end;
    9.22  
    9.23  end;
    9.24  
    9.25 @@ -241,7 +241,6 @@
    9.26    | Markup_Env_Token of string * Input.source
    9.27    | Raw_Token of Input.source;
    9.28  
    9.29 -
    9.30  fun basic_token pred (Basic_Token tok) = pred tok
    9.31    | basic_token _ _ = false;
    9.32  
    9.33 @@ -606,6 +605,24 @@
    9.34  
    9.35  (** concrete antiquotations **)
    9.36  
    9.37 +(* control style *)
    9.38 +
    9.39 +local
    9.40 +
    9.41 +fun control_antiquotation name s1 s2 =
    9.42 +  antiquotation name (Scan.lift Args.cartouche_input)
    9.43 +    (fn {state, ...} => enclose s1 s2 o output_text state {markdown = false});
    9.44 +
    9.45 +in
    9.46 +
    9.47 +val _ =
    9.48 +  Theory.setup
    9.49 +   (control_antiquotation @{binding "emph"} "\\emph{" "}" #>
    9.50 +    control_antiquotation @{binding "bold"} "\\textbf{" "}");
    9.51 +
    9.52 +end;
    9.53 +
    9.54 +
    9.55  (* basic entities *)
    9.56  
    9.57  local
    10.1 --- a/src/Pure/Tools/rail.ML	Sun Oct 18 18:09:48 2015 +0200
    10.2 +++ b/src/Pure/Tools/rail.ML	Sun Oct 18 20:28:29 2015 +0200
    10.3 @@ -85,8 +85,8 @@
    10.4  
    10.5  fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
    10.6  
    10.7 -fun antiq_token (antiq as (ss, {range, ...})) =
    10.8 -  [Token (range, (Antiq antiq, Symbol_Pos.content ss))];
    10.9 +fun antiq_token antiq =
   10.10 +  [Token (#range antiq, (Antiq antiq, Symbol_Pos.content (#body antiq)))];
   10.11  
   10.12  val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
   10.13