# HG changeset patch # User wenzelm # Date 1446849110 -3600 # Node ID 3591274c607eaded1468a06c960668573418883c # Parent 07a903c8cc916a9f165d636910806bf0846802ae more formal treatment of control symbols; diff -r 07a903c8cc91 -r 3591274c607e NEWS --- 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>\...\ is equivalent to @{name \...\} and -\...\ without control symbol is equivalent to @{cartouche \...\}. The +\...\ without control symbol is equivalent to @{cartouche \...\}. +\<^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. diff -r 07a903c8cc91 -r 3591274c607e lib/texinputs/isabelle.sty --- 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}} diff -r 07a903c8cc91 -r 3591274c607e src/Doc/Isar_Ref/Document_Preparation.thy --- 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>\@{\\\\\<^verbatim>\}\) 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>\\<^cartouche>\\\argument_content\\, which - is equivalent to \<^verbatim>\@{cartouche\~\\argument_content\\\<^verbatim>\}\. 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, \\foo_bar + baz \ bazar\\ prints literal - quasi-formal text (unchecked). + A cartouche without special decoration is equivalent to + \<^verbatim>\\<^cartouche>\\\argument_content\\, which is equivalent to + \<^verbatim>\@{cartouche\~\\argument_content\\\<^verbatim>\}\. 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, \\foo_bar + baz \ bazar\\ prints literal quasi-formal text + (unchecked). + + A control symbol \<^verbatim>\\\\<^verbatim>\<^\\name\\<^verbatim>\>\ within the body text, but without a + subsequent cartouche, is equivalent to \<^verbatim>\@{\\name\\<^verbatim>\}\. \begingroup \def\isasymcontrolstart{\isatt{\isacharbackslash\isacharless\isacharcircum}} diff -r 07a903c8cc91 -r 3591274c607e src/Pure/General/antiquote.ML --- 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 <> "\\" andalso s <> "@" andalso Symbol.not_eof s) || - Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\") >> 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 -- diff -r 07a903c8cc91 -r 3591274c607e src/Pure/General/antiquote.scala --- 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)) diff -r 07a903c8cc91 -r 3591274c607e src/Pure/ML/ml_context.ML --- 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; diff -r 07a903c8cc91 -r 3591274c607e src/Pure/Thy/latex.ML --- 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; diff -r 07a903c8cc91 -r 3591274c607e src/Pure/Thy/markdown.ML --- 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 diff -r 07a903c8cc91 -r 3591274c607e src/Pure/Thy/thy_output.ML --- 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