--- a/NEWS Fri Nov 06 23:31:11 2015 +0100
+++ b/NEWS Fri Nov 06 23:31:50 2015 +0100
@@ -79,10 +79,15 @@
* There is a new short form for antiquotations with a single argument
that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and
-\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. The
+\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.
+\<^name> without following cartouche is equivalent to @{name}. The
standard Isabelle fonts provide glyphs to render important control
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
+* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with
+corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
+standard LaTeX macros of the same names.
+
* System option "document_symbols" determines completion of Isabelle
symbols within document source.
@@ -113,13 +118,6 @@
\<^enum> enumerate
\<^descr> description
-* Text may contain control symbols for markup and formatting as follows:
-
- \<^noindent> \noindent
- \<^smallskip> \smallskip
- \<^medskip> \medskip
- \<^bigskip> \bigskip
-
* Command 'text_raw' has been clarified: input text is processed as in
'text' (with antiquotations and control symbols). The key difference is
the lack of the surrounding isabelle markup environment in output.
--- a/lib/texinputs/isabelle.sty Fri Nov 06 23:31:11 2015 +0100
+++ b/lib/texinputs/isabelle.sty Fri Nov 06 23:31:50 2015 +0100
@@ -39,11 +39,6 @@
\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
-\def\isactrlnoindent{\noindent}
-\def\isactrlsmallskip{\smallskip}
-\def\isactrlmedskip{\medskip}
-\def\isactrlbigskip{\bigskip}
-
\newcommand{\isaantiqcontrol}[1]{\isatt{{\char`\\}{\char`\<}{\char`\^}#1{\char`\>}}}
\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Fri Nov 06 23:31:11 2015 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Nov 06 23:31:50 2015 +0100
@@ -134,13 +134,16 @@
surrounding \<^verbatim>\<open>@{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>) works for a single
argument that is a cartouche.
- Omitting the control symbol is also possible: a cartouche without special
- decoration is equivalent to \<^verbatim>\<open>\<^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which
- is equivalent to \<^verbatim>\<open>@{cartouche\<close>~\<open>\<open>argument_content\<close>\<close>\<^verbatim>\<open>}\<close>. The
- special name @{antiquotation_def cartouche} is defined in the context:
- Isabelle/Pure introduces that as an alias to @{antiquotation_ref text}
- (see below). Consequently, \<open>\<open>foo_bar + baz \<le> bazar\<close>\<close> prints literal
- quasi-formal text (unchecked).
+ A cartouche without special decoration is equivalent to
+ \<^verbatim>\<open>\<^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which is equivalent to
+ \<^verbatim>\<open>@{cartouche\<close>~\<open>\<open>argument_content\<close>\<close>\<^verbatim>\<open>}\<close>. The special name
+ @{antiquotation_def cartouche} is defined in the context: Isabelle/Pure
+ introduces that as an alias to @{antiquotation_ref text} (see below).
+ Consequently, \<open>\<open>foo_bar + baz \<le> bazar\<close>\<close> prints literal quasi-formal text
+ (unchecked).
+
+ A control symbol \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> within the body text, but without a
+ subsequent cartouche, is equivalent to \<^verbatim>\<open>@{\<close>\<open>name\<close>\<^verbatim>\<open>}\<close>.
\begingroup
\def\isasymcontrolstart{\isatt{\isacharbackslash\isacharless\isacharcircum}}
--- a/src/Pure/General/antiquote.ML Fri Nov 06 23:31:11 2015 +0100
+++ b/src/Pure/General/antiquote.ML Fri Nov 06 23:31:50 2015 +0100
@@ -80,7 +80,6 @@
Scan.repeats1
(Scan.many1 (fn (s, _) =>
not (Symbol.is_control s) andalso s <> "\\<open>" andalso s <> "@" andalso Symbol.not_eof s) ||
- Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\<open>") >> single ||
$$$ "@" --| Scan.ahead (~$$ "{"));
val scan_antiq_body =
@@ -101,7 +100,10 @@
(case opt_control of
SOME (sym, pos) => ((control_name sym, pos), Symbol_Pos.range ((sym, pos) :: body))
| NONE => (("cartouche", #2 (hd body)), Symbol_Pos.range body));
- in {name = name, range = range, body = body} end);
+ in {name = name, range = range, body = body} end) ||
+ Scan.one (Symbol.is_control o Symbol_Pos.symbol) >>
+ (fn (sym, pos) =>
+ {name = (control_name sym, pos), range = Symbol_Pos.range [(sym, pos)], body = []});
val scan_antiq =
Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
--- a/src/Pure/General/antiquote.scala Fri Nov 06 23:31:11 2015 +0100
+++ b/src/Pure/General/antiquote.scala Fri Nov 06 23:31:50 2015 +0100
@@ -26,11 +26,11 @@
{
private val txt: Parser[String] =
rep1(many1(s => !Symbol.is_control(s) && !Symbol.is_open(s) && s != "@") |
- one(Symbol.is_control) <~ guard(opt_term(one(s => !Symbol.is_open(s)))) |
"@" <~ guard(opt_term(one(s => s != "{")))) ^^ (x => x.mkString)
val control: Parser[String] =
- opt(one(Symbol.is_control)) ~ cartouche ^^ { case Some(x) ~ y => x + y case None ~ x => x }
+ opt(one(Symbol.is_control)) ~ cartouche ^^ { case Some(x) ~ y => x + y case None ~ x => x } |
+ one(Symbol.is_control)
val antiq_other: Parser[String] =
many1(s => s != "\"" && s != "`" && s != "}" && !Symbol.is_open(s) && !Symbol.is_close(s))
--- a/src/Pure/ML/ml_context.ML Fri Nov 06 23:31:11 2015 +0100
+++ b/src/Pure/ML/ml_context.ML Fri Nov 06 23:31:50 2015 +0100
@@ -170,7 +170,8 @@
in (decl #> tokenize range, ctxt') end
else (K ([], [tok]), ctxt)
| expand (Antiquote.Control {name, range, body}) ctxt =
- expand_src range (Token.src name [Token.read_cartouche body]) ctxt
+ expand_src range
+ (Token.src name (if null body then [] else [Token.read_cartouche body])) ctxt
| expand (Antiquote.Antiq {range, body, ...}) ctxt =
expand_src range
(Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt;
--- a/src/Pure/Thy/latex.ML Fri Nov 06 23:31:11 2015 +0100
+++ b/src/Pure/Thy/latex.ML Fri Nov 06 23:31:50 2015 +0100
@@ -10,7 +10,6 @@
val output_known_symbols: (string -> bool) * (string -> bool) ->
Symbol.symbol list -> string
val output_symbols: Symbol.symbol list -> string
- val output_ctrl_symbols: Symbol.symbol list -> string
val output_token: Token.T -> string
val begin_delim: string -> string
val end_delim: string -> string
@@ -99,11 +98,6 @@
| Symbol.Malformed s => error (Symbol.malformed_msg s)
| Symbol.EOF => error "Bad EOF symbol");
-fun output_ctrl_sym sym =
- (case Symbol.decode sym of
- Symbol.Control s => enclose "\\isactrl" " " s
- | _ => sym);
-
in
val output_known_symbols = implode oo (map o output_known_sym);
@@ -119,8 +113,6 @@
enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
(output_symbols (map Symbol_Pos.symbol body)));
-val output_ctrl_symbols = implode o map output_ctrl_sym;
-
end;
--- a/src/Pure/Thy/markdown.ML Fri Nov 06 23:31:11 2015 +0100
+++ b/src/Pure/Thy/markdown.ML Fri Nov 06 23:31:50 2015 +0100
@@ -19,9 +19,9 @@
signature MARKDOWN =
sig
- val is_control: Symbol.symbol -> bool
datatype kind = Itemize | Enumerate | Description
val print_kind: kind -> string
+ val is_control: Symbol.symbol -> bool
type line
val line_source: line -> Antiquote.text_antiquote list
val line_is_item: line -> bool
@@ -39,9 +39,7 @@
structure Markdown: MARKDOWN =
struct
-(* document lines *)
-
-val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
+(* item kinds *)
datatype kind = Itemize | Enumerate | Description;
@@ -49,6 +47,13 @@
| print_kind Enumerate = "enumerate"
| print_kind Description = "description";
+val kinds = [("item", Itemize), ("enum", Enumerate), ("descr", Description)];
+
+val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
+
+
+(* document lines *)
+
datatype line =
Line of
{source: Antiquote.text_antiquote list,
@@ -84,19 +89,22 @@
fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
-val scan_marker =
- Scan.many is_space -- Symbol_Pos.scan_pos --
- Scan.option
- (Symbol_Pos.$$ "\\<^item>" >> K Itemize ||
- Symbol_Pos.$$ "\\<^enum>" >> K Enumerate ||
- Symbol_Pos.$$ "\\<^descr>" >> K Description) --| Scan.many is_space
- >> (fn ((sp, pos), item) => (length sp, item, if is_some item then pos else Position.none));
+fun strip_spaces (Antiquote.Text ss :: rest) =
+ let val (sp, ss') = take_prefix is_space ss
+ in (length sp, if null ss' then rest else Antiquote.Text ss' :: rest) end
+ | strip_spaces source = (0, source);
-fun read_marker (Antiquote.Text ss :: rest) =
- (case Scan.finite Symbol_Pos.stopper scan_marker ss of
- (marker, []) => (marker, rest)
- | (marker, ss') => (marker, Antiquote.Text ss' :: rest))
- | read_marker source = ((0, NONE, Position.none), source);
+fun read_marker source =
+ let val (indent, source') = strip_spaces source in
+ (case source' of
+ (control as Antiquote.Control {name = (name, pos), body = [], ...}) :: rest =>
+ let
+ val item = AList.lookup (op =) kinds name;
+ val item_pos = if is_some item then pos else Position.none;
+ val (_, rest') = strip_spaces (if is_some item then rest else control :: rest);
+ in ((indent, item, item_pos), rest') end
+ | _ => ((indent, NONE, Position.none), source'))
+ end;
in
--- a/src/Pure/Thy/thy_output.ML Fri Nov 06 23:31:11 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML Fri Nov 06 23:31:50 2015 +0100
@@ -177,7 +177,7 @@
fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
| eval_antiquote state (Antiquote.Control {name, body, ...}) =
- eval_antiq state ([], Token.src name [Token.read_cartouche body])
+ eval_antiq state ([], Token.src name (if null body then [] else [Token.read_cartouche body]))
| eval_antiquote state (Antiquote.Antiq {range = (pos, _), body, ...}) =
let
val keywords =
@@ -202,8 +202,7 @@
{symbols = Options.default_bool "document_symbols", delimited = Input.is_delimited source});
val syms = Input.source_explode source;
- val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;
- val output_antiquotes = map output_antiquote #> implode;
+ val output_antiquotes = map (eval_antiquote state) #> implode;
fun output_line line =
(if Markdown.line_is_item line then "\\item " else "") ^
@@ -604,6 +603,16 @@
(** concrete antiquotations **)
+(* control spacing *)
+
+val _ =
+ Theory.setup
+ (antiquotation @{binding noindent} (Scan.succeed ()) (fn _ => fn () => "\\noindent") #>
+ antiquotation @{binding smallskip} (Scan.succeed ()) (fn _ => fn () => "\\smallskip") #>
+ antiquotation @{binding medskip} (Scan.succeed ()) (fn _ => fn () => "\\medskip") #>
+ antiquotation @{binding bigskip} (Scan.succeed ()) (fn _ => fn () => "\\bigskip"));
+
+
(* control style *)
local