--- 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>\<open>...\<close> is
+equivalent to @{"\<^foo>" \<open>...\<close>} 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.
--- 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 (~$$ "\\<open>") >> 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;
--- 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)))
}
--- 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
--- 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
--- 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;
--- 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))))
}
--- 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)));
--- 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 *)