# HG changeset patch # User wenzelm # Date 1377265014 -7200 # Node ID 4e7ddd76e632b20f528f664a30d6a1cbbbfb108f # Parent 1266b6208a5be682f76146fca122ed64fe6dde10 discontinued unused antiquotation blocks; diff -r 1266b6208a5b -r 4e7ddd76e632 lib/texinputs/isabelle.sty --- 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 diff -r 1266b6208a5b -r 4e7ddd76e632 src/Doc/IsarImplementation/ML.thy --- 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 '}' | '\' | '\' + @{syntax_def antiquote}: '@{' nameref args '}' "} Here @{syntax nameref} and @{syntax args} are regular outer syntax diff -r 1266b6208a5b -r 4e7ddd76e632 src/Doc/IsarImplementation/document/style.sty --- 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} diff -r 1266b6208a5b -r 4e7ddd76e632 src/Pure/General/antiquote.ML --- 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 <> "\\" andalso s <> "\\" - 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 --| $$$ "\\"; -val scan_close = Symbol_Pos.scan_pos --| $$$ "\\"; - 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; diff -r 1266b6208a5b -r 4e7ddd76e632 src/Pure/ML/ml_context.ML --- 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; diff -r 1266b6208a5b -r 4e7ddd76e632 src/Pure/ML/ml_lex.ML --- 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); diff -r 1266b6208a5b -r 4e7ddd76e632 src/Pure/Thy/latex.ML --- 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; diff -r 1266b6208a5b -r 4e7ddd76e632 src/Pure/Thy/thy_output.ML --- 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