discontinued unused antiquotation blocks;
authorwenzelm
Fri Aug 23 15:36:54 2013 +0200 (2013-08-23)
changeset 531674e7ddd76e632
parent 53166 1266b6208a5b
child 53168 d998de7f0efc
discontinued unused antiquotation blocks;
lib/texinputs/isabelle.sty
src/Doc/IsarImplementation/ML.thy
src/Doc/IsarImplementation/document/style.sty
src/Pure/General/antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_lex.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/lib/texinputs/isabelle.sty	Fri Aug 23 15:04:00 2013 +0200
     1.2 +++ b/lib/texinputs/isabelle.sty	Fri Aug 23 15:36:54 2013 +0200
     1.3 @@ -37,8 +37,6 @@
     1.4  \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
     1.5  
     1.6  \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
     1.7 -\newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}
     1.8 -\newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}}
     1.9  
    1.10  \newdimen\isa@parindent\newdimen\isa@parskip
    1.11  
     2.1 --- a/src/Doc/IsarImplementation/ML.thy	Fri Aug 23 15:04:00 2013 +0200
     2.2 +++ b/src/Doc/IsarImplementation/ML.thy	Fri Aug 23 15:36:54 2013 +0200
     2.3 @@ -667,7 +667,7 @@
     2.4    ML is augmented by special syntactic entities of the following form:
     2.5  
     2.6    @{rail "
     2.7 -  @{syntax_def antiquote}: '@{' nameref args '}' | '\<lbrace>' | '\<rbrace>'
     2.8 +  @{syntax_def antiquote}: '@{' nameref args '}'
     2.9    "}
    2.10  
    2.11    Here @{syntax nameref} and @{syntax args} are regular outer syntax
     3.1 --- a/src/Doc/IsarImplementation/document/style.sty	Fri Aug 23 15:04:00 2013 +0200
     3.2 +++ b/src/Doc/IsarImplementation/document/style.sty	Fri Aug 23 15:36:54 2013 +0200
     3.3 @@ -24,9 +24,6 @@
     3.4  
     3.5  \renewcommand{\isadigit}[1]{\isamath{#1}}
     3.6  
     3.7 -\renewcommand{\isaantiqopen}{\isasymlbrace}
     3.8 -\renewcommand{\isaantiqclose}{\isasymrbrace}
     3.9 -
    3.10  \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
    3.11  
    3.12  \isafoldtag{FIXME}
     4.1 --- a/src/Pure/General/antiquote.ML	Fri Aug 23 15:04:00 2013 +0200
     4.2 +++ b/src/Pure/General/antiquote.ML	Fri Aug 23 15:36:54 2013 +0200
     4.3 @@ -8,15 +8,11 @@
     4.4  sig
     4.5    datatype 'a antiquote =
     4.6      Text of 'a |
     4.7 -    Antiq of Symbol_Pos.T list * Position.range |
     4.8 -    Open of Position.T |
     4.9 -    Close of Position.T
    4.10 +    Antiq of Symbol_Pos.T list * Position.range
    4.11    val is_text: 'a antiquote -> bool
    4.12    val reports_of: ('a -> Position.report_text list) ->
    4.13      'a antiquote list -> Position.report_text list
    4.14 -  val check_nesting: 'a antiquote list -> unit
    4.15    val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
    4.16 -  val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
    4.17    val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
    4.18    val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
    4.19  end;
    4.20 @@ -28,9 +24,7 @@
    4.21  
    4.22  datatype 'a antiquote =
    4.23    Text of 'a |
    4.24 -  Antiq of Symbol_Pos.T list * Position.range |
    4.25 -  Open of Position.T |
    4.26 -  Close of Position.T;
    4.27 +  Antiq of Symbol_Pos.T list * Position.range;
    4.28  
    4.29  fun is_text (Text _) = true
    4.30    | is_text _ = false;
    4.31 @@ -39,27 +33,7 @@
    4.32  (* reports *)
    4.33  
    4.34  fun reports_of text =
    4.35 -  maps
    4.36 -    (fn Text x => text x
    4.37 -      | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]
    4.38 -      | Open pos => [((pos, Markup.antiq), "")]
    4.39 -      | Close pos => [((pos, Markup.antiq), "")]);
    4.40 -
    4.41 -
    4.42 -(* check_nesting *)
    4.43 -
    4.44 -fun err_unbalanced pos =
    4.45 -  error ("Unbalanced antiquotation block parentheses" ^ Position.here pos);
    4.46 -
    4.47 -fun check_nesting antiqs =
    4.48 -  let
    4.49 -    fun check [] [] = ()
    4.50 -      | check [] (pos :: _) = err_unbalanced pos
    4.51 -      | check (Open pos :: ants) ps = check ants (pos :: ps)
    4.52 -      | check (Close pos :: _) [] = err_unbalanced pos
    4.53 -      | check (Close _ :: ants) (_ :: ps) = check ants ps
    4.54 -      | check (_ :: ants) ps = check ants ps;
    4.55 -  in check antiqs [] end;
    4.56 +  maps (fn Text x => text x | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]);
    4.57  
    4.58  
    4.59  (* scan *)
    4.60 @@ -72,16 +46,12 @@
    4.61  
    4.62  val scan_txt =
    4.63    $$$ "@" --| Scan.ahead (~$$$ "{") ||
    4.64 -  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
    4.65 -    andalso Symbol.is_regular s) >> single;
    4.66 +  Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single;
    4.67  
    4.68  val scan_ant =
    4.69    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
    4.70    Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    4.71  
    4.72 -val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
    4.73 -val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
    4.74 -
    4.75  in
    4.76  
    4.77  val scan_antiq =
    4.78 @@ -90,8 +60,7 @@
    4.79        (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    4.80    >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
    4.81  
    4.82 -fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
    4.83 -val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
    4.84 +val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat);
    4.85  
    4.86  end;
    4.87  
    4.88 @@ -100,7 +69,7 @@
    4.89  
    4.90  fun read (syms, pos) =
    4.91    (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
    4.92 -    SOME xs => (Position.reports_text (reports_of (K []) xs); check_nesting xs; xs)
    4.93 +    SOME xs => (Position.reports_text (reports_of (K []) xs); xs)
    4.94    | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
    4.95  
    4.96  end;
     5.1 --- a/src/Pure/ML/ml_context.ML	Fri Aug 23 15:04:00 2013 +0200
     5.2 +++ b/src/Pure/ML/ml_context.ML	Fri Aug 23 15:36:54 2013 +0200
     5.3 @@ -154,29 +154,24 @@
     5.4        then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
     5.5        else
     5.6          let
     5.7 +          val lex = #1 (Keyword.get_lexicons ());
     5.8 +          fun no_decl _ = ([], []);
     5.9 +
    5.10 +          fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
    5.11 +            | expand (Antiquote.Antiq (ss, range)) ctxt =
    5.12 +                let
    5.13 +                  val (f, _) =
    5.14 +                    antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
    5.15 +                  val (decl, ctxt') = f ctxt;  (* FIXME ?? *)
    5.16 +                  val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
    5.17 +                in (decl', ctxt') end;
    5.18 +
    5.19            val ctxt =
    5.20              (case opt_ctxt of
    5.21                NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos)
    5.22              | SOME ctxt => Context.proof_of ctxt);
    5.23  
    5.24 -          val lex = #1 (Keyword.get_lexicons ());
    5.25 -          fun no_decl _ = ([], []);
    5.26 -
    5.27 -          fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
    5.28 -            | expand (Antiquote.Antiq (ss, range)) (scope, background) =
    5.29 -                let
    5.30 -                  val context = Stack.top scope;
    5.31 -                  val (f, context') =
    5.32 -                    antiquotation (Token.read_antiq lex antiq (ss, #1 range)) context;
    5.33 -                  val (decl, background') = f background;
    5.34 -                  val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
    5.35 -                in (decl', (Stack.map_top (K context') scope, background')) end
    5.36 -            | expand (Antiquote.Open _) (scope, background) =
    5.37 -                (no_decl, (Stack.push scope, background))
    5.38 -            | expand (Antiquote.Close _) (scope, background) =
    5.39 -                (no_decl, (Stack.pop scope, background));
    5.40 -
    5.41 -          val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
    5.42 +          val (decls, ctxt') = fold_map expand ants ctxt;
    5.43            val (ml_env, ml_body) =
    5.44              decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
    5.45          in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
     6.1 --- a/src/Pure/ML/ml_lex.ML	Fri Aug 23 15:04:00 2013 +0200
     6.2 +++ b/src/Pure/ML/ml_lex.ML	Fri Aug 23 15:36:54 2013 +0200
     6.3 @@ -270,7 +270,7 @@
     6.4      scan_ident >> token Ident ||
     6.5      scan_typevar >> token TypeVar));
     6.6  
     6.7 -val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
     6.8 +val scan_antiq = Antiquote.scan_antiq >> Antiquote.Antiq || scan_ml >> Antiquote.Text;
     6.9  
    6.10  fun recover msg =
    6.11   (recover_char ||
    6.12 @@ -304,7 +304,6 @@
    6.13            (SOME (false, fn msg => recover msg >> map Antiquote.Text))
    6.14          |> Source.exhaust
    6.15          |> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token))
    6.16 -        |> tap Antiquote.check_nesting
    6.17          |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
    6.18        handle ERROR msg =>
    6.19          cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos);
     7.1 --- a/src/Pure/Thy/latex.ML	Fri Aug 23 15:04:00 2013 +0200
     7.2 +++ b/src/Pure/Thy/latex.ML	Fri Aug 23 15:36:54 2013 +0200
     7.3 @@ -99,9 +99,7 @@
     7.4    (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
     7.5      | Antiquote.Antiq (ss, _) =>
     7.6          enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
     7.7 -          (output_symbols (map Symbol_Pos.symbol ss))
     7.8 -    | Antiquote.Open _ => "{\\isaantiqopen}"
     7.9 -    | Antiquote.Close _ => "{\\isaantiqclose}");
    7.10 +          (output_symbols (map Symbol_Pos.symbol ss)));
    7.11  
    7.12  end;
    7.13  
     8.1 --- a/src/Pure/Thy/thy_output.ML	Fri Aug 23 15:04:00 2013 +0200
     8.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 23 15:36:54 2013 +0200
     8.3 @@ -178,9 +178,7 @@
     8.4  fun eval_antiquote lex state (txt, pos) =
     8.5    let
     8.6      fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
     8.7 -      | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq
     8.8 -      | expand (Antiquote.Open _) = ""
     8.9 -      | expand (Antiquote.Close _) = "";
    8.10 +      | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq;
    8.11      val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
    8.12    in
    8.13      if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then