--- a/lib/texinputs/isabelle.sty Fri Aug 23 15:04:00 2013 +0200
+++ b/lib/texinputs/isabelle.sty Fri Aug 23 15:36:54 2013 +0200
@@ -37,8 +37,6 @@
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
-\newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}
-\newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}}
\newdimen\isa@parindent\newdimen\isa@parskip
--- a/src/Doc/IsarImplementation/ML.thy Fri Aug 23 15:04:00 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy Fri Aug 23 15:36:54 2013 +0200
@@ -667,7 +667,7 @@
ML is augmented by special syntactic entities of the following form:
@{rail "
- @{syntax_def antiquote}: '@{' nameref args '}' | '\<lbrace>' | '\<rbrace>'
+ @{syntax_def antiquote}: '@{' nameref args '}'
"}
Here @{syntax nameref} and @{syntax args} are regular outer syntax
--- a/src/Doc/IsarImplementation/document/style.sty Fri Aug 23 15:04:00 2013 +0200
+++ b/src/Doc/IsarImplementation/document/style.sty Fri Aug 23 15:36:54 2013 +0200
@@ -24,9 +24,6 @@
\renewcommand{\isadigit}[1]{\isamath{#1}}
-\renewcommand{\isaantiqopen}{\isasymlbrace}
-\renewcommand{\isaantiqclose}{\isasymrbrace}
-
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
\isafoldtag{FIXME}
--- a/src/Pure/General/antiquote.ML Fri Aug 23 15:04:00 2013 +0200
+++ b/src/Pure/General/antiquote.ML Fri Aug 23 15:36:54 2013 +0200
@@ -8,15 +8,11 @@
sig
datatype 'a antiquote =
Text of 'a |
- Antiq of Symbol_Pos.T list * Position.range |
- Open of Position.T |
- Close of Position.T
+ Antiq of Symbol_Pos.T list * Position.range
val is_text: 'a antiquote -> bool
val reports_of: ('a -> Position.report_text list) ->
'a antiquote list -> Position.report_text list
- val check_nesting: 'a antiquote list -> unit
val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
- val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
end;
@@ -28,9 +24,7 @@
datatype 'a antiquote =
Text of 'a |
- Antiq of Symbol_Pos.T list * Position.range |
- Open of Position.T |
- Close of Position.T;
+ Antiq of Symbol_Pos.T list * Position.range;
fun is_text (Text _) = true
| is_text _ = false;
@@ -39,27 +33,7 @@
(* reports *)
fun reports_of text =
- maps
- (fn Text x => text x
- | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]
- | Open pos => [((pos, Markup.antiq), "")]
- | Close pos => [((pos, Markup.antiq), "")]);
-
-
-(* check_nesting *)
-
-fun err_unbalanced pos =
- error ("Unbalanced antiquotation block parentheses" ^ Position.here pos);
-
-fun check_nesting antiqs =
- let
- fun check [] [] = ()
- | check [] (pos :: _) = err_unbalanced pos
- | check (Open pos :: ants) ps = check ants (pos :: ps)
- | check (Close pos :: _) [] = err_unbalanced pos
- | check (Close _ :: ants) (_ :: ps) = check ants ps
- | check (_ :: ants) ps = check ants ps;
- in check antiqs [] end;
+ maps (fn Text x => text x | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]);
(* scan *)
@@ -72,16 +46,12 @@
val scan_txt =
$$$ "@" --| Scan.ahead (~$$$ "{") ||
- Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
- andalso Symbol.is_regular s) >> single;
+ Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single;
val scan_ant =
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
-val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
-val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
-
in
val scan_antiq =
@@ -90,8 +60,7 @@
(Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
>> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
-fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
-val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
+val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat);
end;
@@ -100,7 +69,7 @@
fun read (syms, pos) =
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
- SOME xs => (Position.reports_text (reports_of (K []) xs); check_nesting xs; xs)
+ SOME xs => (Position.reports_text (reports_of (K []) xs); xs)
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
end;
--- a/src/Pure/ML/ml_context.ML Fri Aug 23 15:04:00 2013 +0200
+++ b/src/Pure/ML/ml_context.ML Fri Aug 23 15:36:54 2013 +0200
@@ -154,29 +154,24 @@
then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
else
let
+ val lex = #1 (Keyword.get_lexicons ());
+ fun no_decl _ = ([], []);
+
+ fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
+ | expand (Antiquote.Antiq (ss, range)) ctxt =
+ let
+ val (f, _) =
+ antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
+ val (decl, ctxt') = f ctxt; (* FIXME ?? *)
+ val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
+ in (decl', ctxt') end;
+
val ctxt =
(case opt_ctxt of
NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos)
| SOME ctxt => Context.proof_of ctxt);
- val lex = #1 (Keyword.get_lexicons ());
- fun no_decl _ = ([], []);
-
- fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
- | expand (Antiquote.Antiq (ss, range)) (scope, background) =
- let
- val context = Stack.top scope;
- val (f, context') =
- antiquotation (Token.read_antiq lex antiq (ss, #1 range)) context;
- val (decl, background') = f background;
- val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
- in (decl', (Stack.map_top (K context') scope, background')) end
- | expand (Antiquote.Open _) (scope, background) =
- (no_decl, (Stack.push scope, background))
- | expand (Antiquote.Close _) (scope, background) =
- (no_decl, (Stack.pop scope, background));
-
- val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
+ val (decls, ctxt') = fold_map expand ants ctxt;
val (ml_env, ml_body) =
decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
--- a/src/Pure/ML/ml_lex.ML Fri Aug 23 15:04:00 2013 +0200
+++ b/src/Pure/ML/ml_lex.ML Fri Aug 23 15:36:54 2013 +0200
@@ -270,7 +270,7 @@
scan_ident >> token Ident ||
scan_typevar >> token TypeVar));
-val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
+val scan_antiq = Antiquote.scan_antiq >> Antiquote.Antiq || scan_ml >> Antiquote.Text;
fun recover msg =
(recover_char ||
@@ -304,7 +304,6 @@
(SOME (false, fn msg => recover msg >> map Antiquote.Text))
|> Source.exhaust
|> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token))
- |> tap Antiquote.check_nesting
|> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
handle ERROR msg =>
cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos);
--- a/src/Pure/Thy/latex.ML Fri Aug 23 15:04:00 2013 +0200
+++ b/src/Pure/Thy/latex.ML Fri Aug 23 15:36:54 2013 +0200
@@ -99,9 +99,7 @@
(fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
| Antiquote.Antiq (ss, _) =>
enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
- (output_symbols (map Symbol_Pos.symbol ss))
- | Antiquote.Open _ => "{\\isaantiqopen}"
- | Antiquote.Close _ => "{\\isaantiqclose}");
+ (output_symbols (map Symbol_Pos.symbol ss)));
end;
--- a/src/Pure/Thy/thy_output.ML Fri Aug 23 15:04:00 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Aug 23 15:36:54 2013 +0200
@@ -178,9 +178,7 @@
fun eval_antiquote lex state (txt, pos) =
let
fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
- | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq
- | expand (Antiquote.Open _) = ""
- | expand (Antiquote.Close _) = "";
+ | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq;
val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
in
if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then