# HG changeset patch # User wenzelm # Date 1445181864 -7200 # Node ID 9d4c08af61b8bf2b4841c07d7d58cc1f630cc5b6 # Parent c42960228a81796a8683b33143e1920fa165dcfb support control symbol antiquotations; diff -r c42960228a81 -r 9d4c08af61b8 NEWS --- a/NEWS Sun Oct 18 17:20:20 2015 +0200 +++ b/NEWS Sun Oct 18 17:24:24 2015 +0200 @@ -22,9 +22,8 @@ * Toplevel theorem statement 'proposition' is another alias for 'theorem'. -* HTML presentation uses the standard IsabelleText font and Unicode -rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former -print mode "HTML" looses its special meaning. +* There is a new short form of antiquotations: \<^foo>\...\ is +equivalent to @{"\<^foo>" \...\} for control symbols. *** Prover IDE -- Isabelle/Scala/jEdit *** @@ -57,6 +56,10 @@ *** Document preparation *** +* HTML presentation uses the standard IsabelleText font and Unicode +rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former +print mode "HTML" looses its special meaning. + * Commands 'paragraph' and 'subparagraph' provide additional section headings. Thus there are 6 levels of standard headings, as in HTML. diff -r c42960228a81 -r 9d4c08af61b8 src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Sun Oct 18 17:20:20 2015 +0200 +++ b/src/Pure/General/antiquote.ML Sun Oct 18 17:24:24 2015 +0200 @@ -7,11 +7,13 @@ signature ANTIQUOTE = sig type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range} - datatype 'a antiquote = Text of 'a | Antiq of antiq + datatype 'a antiquote = + Text of 'a | Control of Symbol_Pos.T * Symbol_Pos.T list | Antiq of antiq type text_antiquote = Symbol_Pos.T list antiquote val range: text_antiquote list -> Position.range val split_lines: text_antiquote list -> text_antiquote list list val antiq_reports: 'a antiquote list -> Position.report list + val scan_control: Symbol_Pos.T list -> (Symbol_Pos.T * Symbol_Pos.T list) * Symbol_Pos.T list val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list val read': Position.T -> Symbol_Pos.T list -> text_antiquote list @@ -24,11 +26,13 @@ (* datatype antiquote *) type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}; -datatype 'a antiquote = Text of 'a | Antiq of antiq; +datatype 'a antiquote = + Text of 'a | Control of Symbol_Pos.T * Symbol_Pos.T list | Antiq of antiq; type text_antiquote = Symbol_Pos.T list antiquote; fun antiquote_range (Text ss) = Symbol_Pos.range ss + | antiquote_range (Control (s, ss)) = Symbol_Pos.range (s :: ss) | antiquote_range (Antiq (_, {range, ...})) = range; fun range ants = @@ -55,12 +59,13 @@ (* reports *) fun antiq_reports ants = ants |> maps - (fn Antiq (_, {start, stop, range = (pos, _)}) => - [(start, Markup.antiquote), - (stop, Markup.antiquote), - (pos, Markup.antiquoted), - (pos, Markup.language_antiquotation)] - | _ => []); + (fn Text _ => [] + | Control (s, ss) => [(#1 (Symbol_Pos.range (s :: ss)), Markup.antiquoted)] + | Antiq (_, {start, stop, range = (pos, _)}) => + [(start, Markup.antiquote), + (stop, Markup.antiquote), + (pos, Markup.antiquoted), + (pos, Markup.language_antiquotation)]); (* scan *) @@ -72,8 +77,10 @@ val err_prefix = "Antiquotation lexical error: "; val scan_txt = - Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") || - Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.not_eof s)) >> flat; + Scan.repeat1 + (Scan.many1 (fn (s, _) => not (Symbol.is_control s) andalso s <> "@" andalso Symbol.not_eof s) || + Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\") >> single || + $$$ "@" --| Scan.ahead (~$$ "{")) >> flat; val scan_antiq_body = Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || @@ -82,6 +89,10 @@ in +val scan_control = + Scan.one (Symbol.is_control o Symbol_Pos.symbol) -- + (Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2); + val scan_antiq = Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos -- Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") @@ -92,7 +103,8 @@ stop = Position.set_range (pos3, pos4), range = Position.range pos1 pos4})); -val scan_antiquote = scan_antiq >> Antiq || scan_txt >> Text; +val scan_antiquote = + scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text; end; diff -r c42960228a81 -r 9d4c08af61b8 src/Pure/General/antiquote.scala --- a/src/Pure/General/antiquote.scala Sun Oct 18 17:20:20 2015 +0200 +++ b/src/Pure/General/antiquote.scala Sun Oct 18 17:24:24 2015 +0200 @@ -14,6 +14,7 @@ { sealed abstract class Antiquote case class Text(source: String) extends Antiquote + case class Control(source: String) extends Antiquote case class Antiq(source: String) extends Antiquote @@ -24,7 +25,12 @@ trait Parsers extends Scan.Parsers { private val txt: Parser[String] = - rep1("@" ~ guard(one(s => s != "{")) | many1(s => s != "@")) ^^ (x => x.mkString) + rep1(many1(s => !Symbol.is_control(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] = + one(Symbol.is_control) ~ cartouche ^^ { case x ~ y => x + y } val antiq_other: Parser[String] = many1(s => s != "\"" && s != "`" && s != "}" && !Symbol.is_open(s) && !Symbol.is_close(s)) @@ -36,7 +42,7 @@ "@{" ~ rep(antiq_body) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z } val antiquote: Parser[Antiquote] = - antiq ^^ (x => Antiq(x)) | txt ^^ (x => Text(x)) + control ^^ (x => Control(x)) | (antiq ^^ (x => Antiq(x)) | txt ^^ (x => Text(x))) } diff -r c42960228a81 -r 9d4c08af61b8 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Sun Oct 18 17:20:20 2015 +0200 +++ b/src/Pure/Isar/token.ML Sun Oct 18 17:24:24 2015 +0200 @@ -96,6 +96,7 @@ val source_strict: Keyword.keywords -> Position.T -> (Symbol.symbol, 'a) Source.source -> (T, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source + val read_cartouche: Symbol_Pos.T list -> T val explode: Keyword.keywords -> Position.T -> string -> T list val make: (int * int) * string -> Position.T -> T * Position.T type 'a parser = T list -> 'a * T list @@ -633,6 +634,11 @@ fun source keywords pos src = Symbol_Pos.source pos src |> source' false keywords; fun source_strict keywords pos src = Symbol_Pos.source pos src |> source' true keywords; +fun read_cartouche syms = + (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of + SOME tok => tok + | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms)))); + end; @@ -668,7 +674,7 @@ type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list); -(* read source *) +(* read antiquotation source *) fun read_no_commands keywords scan syms = Source.of_list syms diff -r c42960228a81 -r 9d4c08af61b8 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Sun Oct 18 17:20:20 2015 +0200 +++ b/src/Pure/ML/ml_context.ML Sun Oct 18 17:24:24 2015 +0200 @@ -133,6 +133,7 @@ fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end"); fun expanding (Antiquote.Text tok) = ML_Lex.is_cartouche tok + | expanding (Antiquote.Control _) = true | expanding (Antiquote.Antiq _) = true; fun eval_antiquotes (ants, pos) opt_context = @@ -150,13 +151,11 @@ let fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range)); - fun expand (Antiquote.Antiq (ss, {range, ...})) ctxt = - let - val keywords = Thy_Header.get_keywords' ctxt; - val (decl, ctxt') = - apply_antiquotation (Token.read_antiq keywords antiq (ss, #1 range)) ctxt; - in (decl #> tokenize range, ctxt') end - | expand (Antiquote.Text tok) ctxt = + fun expand_src range src ctxt = + let val (decl, ctxt') = apply_antiquotation src ctxt + in (decl #> tokenize range, ctxt') end; + + fun expand (Antiquote.Text tok) ctxt = if ML_Lex.is_cartouche tok then let val range = ML_Lex.range_of tok; @@ -169,7 +168,13 @@ ("Input.source true " ^ ML_Syntax.print_string text ^ " " ^ ML_Syntax.atomic (ML_Syntax.print_range range)) ctxt; in (decl #> tokenize range, ctxt') end - else (K ([], [tok]), ctxt); + else (K ([], [tok]), ctxt) + | expand (Antiquote.Control (s, ss)) ctxt = + let val range = Symbol_Pos.range (s :: ss) + in expand_src range (Token.src s [Token.read_cartouche ss]) ctxt end + | expand (Antiquote.Antiq (ss, {range, ...})) ctxt = + let val keywords = Thy_Header.get_keywords' ctxt + in expand_src range (Token.read_antiq keywords antiq (ss, #1 range)) ctxt end; val ctxt = (case opt_ctxt of diff -r c42960228a81 -r 9d4c08af61b8 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Sun Oct 18 17:20:20 2015 +0200 +++ b/src/Pure/ML/ml_lex.ML Sun Oct 18 17:24:24 2015 +0200 @@ -293,6 +293,7 @@ val scan_sml = scan_ml >> Antiquote.Text; val scan_ml_antiq = + Antiquote.scan_control >> Antiquote.Control || Antiquote.scan_antiq >> Antiquote.Antiq || Symbol_Pos.scan_cartouche err_prefix >> (Antiquote.Text o token Cartouche) || scan_ml >> Antiquote.Text; diff -r c42960228a81 -r 9d4c08af61b8 src/Pure/ML/ml_lex.scala --- a/src/Pure/ML/ml_lex.scala Sun Oct 18 17:20:20 2015 +0200 +++ b/src/Pure/ML/ml_lex.scala Sun Oct 18 17:24:24 2015 +0200 @@ -52,6 +52,7 @@ val SPACE = Value("white space") val CARTOUCHE = Value("text cartouche") val COMMENT = Value("comment text") + val CONTROL = Value("control symbol antiquotation") val ANTIQ = Value("antiquotation") val ANTIQ_START = Value("antiquotation: start") val ANTIQ_STOP = Value("antiquotation: stop") @@ -211,12 +212,13 @@ val keyword = literal(lexicon) ^^ (x => Token(Kind.KEYWORD, x)) + val ml_control = control ^^ (x => Token(Kind.CONTROL, x)) val ml_antiq = antiq ^^ (x => Token(Kind.ANTIQ, x)) val bad = one(_ => true) ^^ (x => Token(Kind.ERROR, x)) - space | (recover_delimited | (ml_antiq | - (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad))) + space | (recover_delimited | (ml_control | (ml_antiq | + (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad)))) } diff -r c42960228a81 -r 9d4c08af61b8 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Sun Oct 18 17:20:20 2015 +0200 +++ b/src/Pure/Thy/latex.ML Sun Oct 18 17:24:24 2015 +0200 @@ -112,6 +112,7 @@ val output_syms_antiq = (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss) + | Antiquote.Control (s, ss) => output_symbols (map Symbol_Pos.symbol (s :: ss)) | Antiquote.Antiq (ss, _) => enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))); diff -r c42960228a81 -r 9d4c08af61b8 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sun Oct 18 17:20:20 2015 +0200 +++ b/src/Pure/Thy/thy_output.ML Sun Oct 18 17:24:24 2015 +0200 @@ -161,7 +161,23 @@ (* eval antiquote *) +local + +fun eval_antiq state (opts, src) = + let + val preview_ctxt = fold option opts (Toplevel.presentation_context_of state); + val print_ctxt = Context_Position.set_visible false preview_ctxt; + + fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) (); + val _ = cmd preview_ctxt; + val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes; + in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end; + +in + fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss + | eval_antiquote state (Antiquote.Control (control, arg)) = + eval_antiq state ([], Token.src control [Token.read_cartouche arg]) | eval_antiquote state (Antiquote.Antiq (ss, {range = (pos, _), ...})) = let val keywords = @@ -170,15 +186,9 @@ | NONE => error ("Unknown context -- cannot expand document antiquotations" ^ Position.here pos)); - - val (opts, src) = Token.read_antiq keywords antiq (ss, pos); - fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) (); + in eval_antiq state (Token.read_antiq keywords antiq (ss, pos)) end; - val preview_ctxt = fold option opts (Toplevel.presentation_context_of state); - val print_ctxt = Context_Position.set_visible false preview_ctxt; - val _ = cmd preview_ctxt; - val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes; - in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end; +end; (* output text *)