more formal treatment of control symbols;
authorwenzelm
Fri Nov 06 23:31:50 2015 +0100 (2015-11-06)
changeset 615953591274c607e
parent 61594 07a903c8cc91
child 61596 8323b8e21fe9
more formal treatment of control symbols;
NEWS
lib/texinputs/isabelle.sty
src/Doc/Isar_Ref/Document_Preparation.thy
src/Pure/General/antiquote.ML
src/Pure/General/antiquote.scala
src/Pure/ML/ml_context.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/markdown.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Fri Nov 06 23:31:11 2015 +0100
     1.2 +++ b/NEWS	Fri Nov 06 23:31:50 2015 +0100
     1.3 @@ -79,10 +79,15 @@
     1.4  
     1.5  * There is a new short form for antiquotations with a single argument
     1.6  that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and
     1.7 -\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. The
     1.8 +\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.
     1.9 +\<^name> without following cartouche is equivalent to @{name}. The
    1.10  standard Isabelle fonts provide glyphs to render important control
    1.11  symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
    1.12  
    1.13 +* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with
    1.14 +corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
    1.15 +standard LaTeX macros of the same names.
    1.16 +
    1.17  * System option "document_symbols" determines completion of Isabelle
    1.18  symbols within document source.
    1.19  
    1.20 @@ -113,13 +118,6 @@
    1.21    \<^enum>  enumerate
    1.22    \<^descr>  description
    1.23  
    1.24 -* Text may contain control symbols for markup and formatting as follows:
    1.25 -
    1.26 -  \<^noindent>   \noindent
    1.27 -  \<^smallskip>   \smallskip
    1.28 -  \<^medskip>   \medskip
    1.29 -  \<^bigskip>   \bigskip
    1.30 -
    1.31  * Command 'text_raw' has been clarified: input text is processed as in
    1.32  'text' (with antiquotations and control symbols). The key difference is
    1.33  the lack of the surrounding isabelle markup environment in output.
     2.1 --- a/lib/texinputs/isabelle.sty	Fri Nov 06 23:31:11 2015 +0100
     2.2 +++ b/lib/texinputs/isabelle.sty	Fri Nov 06 23:31:50 2015 +0100
     2.3 @@ -39,11 +39,6 @@
     2.4  \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
     2.5  \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
     2.6  
     2.7 -\def\isactrlnoindent{\noindent}
     2.8 -\def\isactrlsmallskip{\smallskip}
     2.9 -\def\isactrlmedskip{\medskip}
    2.10 -\def\isactrlbigskip{\bigskip}
    2.11 -
    2.12  \newcommand{\isaantiqcontrol}[1]{\isatt{{\char`\\}{\char`\<}{\char`\^}#1{\char`\>}}}
    2.13  \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
    2.14  
     3.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Nov 06 23:31:11 2015 +0100
     3.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Nov 06 23:31:50 2015 +0100
     3.3 @@ -134,13 +134,16 @@
     3.4    surrounding \<^verbatim>\<open>@{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>) works for a single
     3.5    argument that is a cartouche.
     3.6  
     3.7 -  Omitting the control symbol is also possible: a cartouche without special
     3.8 -  decoration is equivalent to \<^verbatim>\<open>\<^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which
     3.9 -  is equivalent to \<^verbatim>\<open>@{cartouche\<close>~\<open>\<open>argument_content\<close>\<close>\<^verbatim>\<open>}\<close>. The
    3.10 -  special name @{antiquotation_def cartouche} is defined in the context:
    3.11 -  Isabelle/Pure introduces that as an alias to @{antiquotation_ref text}
    3.12 -  (see below). Consequently, \<open>\<open>foo_bar + baz \<le> bazar\<close>\<close> prints literal
    3.13 -  quasi-formal text (unchecked).
    3.14 +  A cartouche without special decoration is equivalent to
    3.15 +  \<^verbatim>\<open>\<^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which is equivalent to
    3.16 +  \<^verbatim>\<open>@{cartouche\<close>~\<open>\<open>argument_content\<close>\<close>\<^verbatim>\<open>}\<close>. The special name
    3.17 +  @{antiquotation_def cartouche} is defined in the context: Isabelle/Pure
    3.18 +  introduces that as an alias to @{antiquotation_ref text} (see below).
    3.19 +  Consequently, \<open>\<open>foo_bar + baz \<le> bazar\<close>\<close> prints literal quasi-formal text
    3.20 +  (unchecked).
    3.21 +
    3.22 +  A control symbol \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> within the body text, but without a
    3.23 +  subsequent cartouche, is equivalent to \<^verbatim>\<open>@{\<close>\<open>name\<close>\<^verbatim>\<open>}\<close>.
    3.24  
    3.25    \begingroup
    3.26    \def\isasymcontrolstart{\isatt{\isacharbackslash\isacharless\isacharcircum}}
     4.1 --- a/src/Pure/General/antiquote.ML	Fri Nov 06 23:31:11 2015 +0100
     4.2 +++ b/src/Pure/General/antiquote.ML	Fri Nov 06 23:31:50 2015 +0100
     4.3 @@ -80,7 +80,6 @@
     4.4    Scan.repeats1
     4.5     (Scan.many1 (fn (s, _) =>
     4.6        not (Symbol.is_control s) andalso s <> "\\<open>" andalso s <> "@" andalso Symbol.not_eof s) ||
     4.7 -    Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\<open>") >> single ||
     4.8      $$$ "@" --| Scan.ahead (~$$ "{"));
     4.9  
    4.10  val scan_antiq_body =
    4.11 @@ -101,7 +100,10 @@
    4.12            (case opt_control of
    4.13              SOME (sym, pos) => ((control_name sym, pos), Symbol_Pos.range ((sym, pos) :: body))
    4.14            | NONE => (("cartouche", #2 (hd body)), Symbol_Pos.range body));
    4.15 -      in {name = name, range = range, body = body} end);
    4.16 +      in {name = name, range = range, body = body} end) ||
    4.17 +  Scan.one (Symbol.is_control o Symbol_Pos.symbol) >>
    4.18 +    (fn (sym, pos) =>
    4.19 +      {name = (control_name sym, pos), range = Symbol_Pos.range [(sym, pos)], body = []});
    4.20  
    4.21  val scan_antiq =
    4.22    Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
     5.1 --- a/src/Pure/General/antiquote.scala	Fri Nov 06 23:31:11 2015 +0100
     5.2 +++ b/src/Pure/General/antiquote.scala	Fri Nov 06 23:31:50 2015 +0100
     5.3 @@ -26,11 +26,11 @@
     5.4    {
     5.5      private val txt: Parser[String] =
     5.6        rep1(many1(s => !Symbol.is_control(s) && !Symbol.is_open(s) && s != "@") |
     5.7 -        one(Symbol.is_control) <~ guard(opt_term(one(s => !Symbol.is_open(s)))) |
     5.8          "@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)
     5.9  
    5.10      val control: Parser[String] =
    5.11 -      opt(one(Symbol.is_control)) ~ cartouche ^^ { case Some(x) ~ y => x + y case None ~ x => x }
    5.12 +      opt(one(Symbol.is_control)) ~ cartouche ^^ { case Some(x) ~ y => x + y case None ~ x => x } |
    5.13 +      one(Symbol.is_control)
    5.14  
    5.15      val antiq_other: Parser[String] =
    5.16        many1(s => s != "\"" && s != "`" && s != "}" && !Symbol.is_open(s) && !Symbol.is_close(s))
     6.1 --- a/src/Pure/ML/ml_context.ML	Fri Nov 06 23:31:11 2015 +0100
     6.2 +++ b/src/Pure/ML/ml_context.ML	Fri Nov 06 23:31:50 2015 +0100
     6.3 @@ -170,7 +170,8 @@
     6.4                    in (decl #> tokenize range, ctxt') end
     6.5                  else (K ([], [tok]), ctxt)
     6.6              | expand (Antiquote.Control {name, range, body}) ctxt =
     6.7 -                expand_src range (Token.src name [Token.read_cartouche body]) ctxt
     6.8 +                expand_src range
     6.9 +                  (Token.src name (if null body then [] else [Token.read_cartouche body])) ctxt
    6.10              | expand (Antiquote.Antiq {range, body, ...}) ctxt =
    6.11                  expand_src range
    6.12                    (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt;
     7.1 --- a/src/Pure/Thy/latex.ML	Fri Nov 06 23:31:11 2015 +0100
     7.2 +++ b/src/Pure/Thy/latex.ML	Fri Nov 06 23:31:50 2015 +0100
     7.3 @@ -10,7 +10,6 @@
     7.4    val output_known_symbols: (string -> bool) * (string -> bool) ->
     7.5      Symbol.symbol list -> string
     7.6    val output_symbols: Symbol.symbol list -> string
     7.7 -  val output_ctrl_symbols: Symbol.symbol list -> string
     7.8    val output_token: Token.T -> string
     7.9    val begin_delim: string -> string
    7.10    val end_delim: string -> string
    7.11 @@ -99,11 +98,6 @@
    7.12    | Symbol.Malformed s => error (Symbol.malformed_msg s)
    7.13    | Symbol.EOF => error "Bad EOF symbol");
    7.14  
    7.15 -fun output_ctrl_sym sym =
    7.16 -  (case Symbol.decode sym of
    7.17 -    Symbol.Control s => enclose "\\isactrl" " " s
    7.18 -  | _ => sym);
    7.19 -
    7.20  in
    7.21  
    7.22  val output_known_symbols = implode oo (map o output_known_sym);
    7.23 @@ -119,8 +113,6 @@
    7.24          enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
    7.25            (output_symbols (map Symbol_Pos.symbol body)));
    7.26  
    7.27 -val output_ctrl_symbols = implode o map output_ctrl_sym;
    7.28 -
    7.29  end;
    7.30  
    7.31  
     8.1 --- a/src/Pure/Thy/markdown.ML	Fri Nov 06 23:31:11 2015 +0100
     8.2 +++ b/src/Pure/Thy/markdown.ML	Fri Nov 06 23:31:50 2015 +0100
     8.3 @@ -19,9 +19,9 @@
     8.4  
     8.5  signature MARKDOWN =
     8.6  sig
     8.7 -  val is_control: Symbol.symbol -> bool
     8.8    datatype kind = Itemize | Enumerate | Description
     8.9    val print_kind: kind -> string
    8.10 +  val is_control: Symbol.symbol -> bool
    8.11    type line
    8.12    val line_source: line -> Antiquote.text_antiquote list
    8.13    val line_is_item: line -> bool
    8.14 @@ -39,9 +39,7 @@
    8.15  structure Markdown: MARKDOWN =
    8.16  struct
    8.17  
    8.18 -(* document lines *)
    8.19 -
    8.20 -val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
    8.21 +(* item kinds *)
    8.22  
    8.23  datatype kind = Itemize | Enumerate | Description;
    8.24  
    8.25 @@ -49,6 +47,13 @@
    8.26    | print_kind Enumerate = "enumerate"
    8.27    | print_kind Description = "description";
    8.28  
    8.29 +val kinds = [("item", Itemize), ("enum", Enumerate), ("descr", Description)];
    8.30 +
    8.31 +val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
    8.32 +
    8.33 +
    8.34 +(* document lines *)
    8.35 +
    8.36  datatype line =
    8.37    Line of
    8.38     {source: Antiquote.text_antiquote list,
    8.39 @@ -84,19 +89,22 @@
    8.40  fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
    8.41  val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
    8.42  
    8.43 -val scan_marker =
    8.44 -  Scan.many is_space -- Symbol_Pos.scan_pos --
    8.45 -  Scan.option
    8.46 -   (Symbol_Pos.$$ "\\<^item>" >> K Itemize ||
    8.47 -    Symbol_Pos.$$ "\\<^enum>" >> K Enumerate ||
    8.48 -    Symbol_Pos.$$ "\\<^descr>" >> K Description) --| Scan.many is_space
    8.49 -  >> (fn ((sp, pos), item) => (length sp, item, if is_some item then pos else Position.none));
    8.50 +fun strip_spaces (Antiquote.Text ss :: rest) =
    8.51 +      let val (sp, ss') = take_prefix is_space ss
    8.52 +      in (length sp, if null ss' then rest else Antiquote.Text ss' :: rest) end
    8.53 +  | strip_spaces source = (0, source);
    8.54  
    8.55 -fun read_marker (Antiquote.Text ss :: rest) =
    8.56 -      (case Scan.finite Symbol_Pos.stopper scan_marker ss of
    8.57 -        (marker, []) => (marker, rest)
    8.58 -      | (marker, ss') => (marker, Antiquote.Text ss' :: rest))
    8.59 -  | read_marker source = ((0, NONE, Position.none), source);
    8.60 +fun read_marker source =
    8.61 +  let val (indent, source') = strip_spaces source in
    8.62 +    (case source' of
    8.63 +      (control as Antiquote.Control {name = (name, pos), body = [], ...}) :: rest =>
    8.64 +        let
    8.65 +          val item = AList.lookup (op =) kinds name;
    8.66 +          val item_pos = if is_some item then pos else Position.none;
    8.67 +          val (_, rest') = strip_spaces (if is_some item then rest else control :: rest);
    8.68 +        in ((indent, item, item_pos), rest') end
    8.69 +    | _ => ((indent, NONE, Position.none), source'))
    8.70 +  end;
    8.71  
    8.72  in
    8.73  
     9.1 --- a/src/Pure/Thy/thy_output.ML	Fri Nov 06 23:31:11 2015 +0100
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Nov 06 23:31:50 2015 +0100
     9.3 @@ -177,7 +177,7 @@
     9.4  
     9.5  fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
     9.6    | eval_antiquote state (Antiquote.Control {name, body, ...}) =
     9.7 -      eval_antiq state ([], Token.src name [Token.read_cartouche body])
     9.8 +      eval_antiq state ([], Token.src name (if null body then [] else [Token.read_cartouche body]))
     9.9    | eval_antiquote state (Antiquote.Antiq {range = (pos, _), body, ...}) =
    9.10        let
    9.11          val keywords =
    9.12 @@ -202,8 +202,7 @@
    9.13            {symbols = Options.default_bool "document_symbols", delimited = Input.is_delimited source});
    9.14      val syms = Input.source_explode source;
    9.15  
    9.16 -    val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;
    9.17 -    val output_antiquotes = map output_antiquote #> implode;
    9.18 +    val output_antiquotes = map (eval_antiquote state) #> implode;
    9.19  
    9.20      fun output_line line =
    9.21        (if Markdown.line_is_item line then "\\item " else "") ^
    9.22 @@ -604,6 +603,16 @@
    9.23  
    9.24  (** concrete antiquotations **)
    9.25  
    9.26 +(* control spacing *)
    9.27 +
    9.28 +val _ =
    9.29 +  Theory.setup
    9.30 +   (antiquotation @{binding noindent} (Scan.succeed ()) (fn _ => fn () => "\\noindent") #>
    9.31 +    antiquotation @{binding smallskip} (Scan.succeed ()) (fn _ => fn () => "\\smallskip") #>
    9.32 +    antiquotation @{binding medskip} (Scan.succeed ()) (fn _ => fn () => "\\medskip") #>
    9.33 +    antiquotation @{binding bigskip} (Scan.succeed ()) (fn _ => fn () => "\\bigskip"));
    9.34 +
    9.35 +
    9.36  (* control style *)
    9.37  
    9.38  local