parameterized datatype antiquote and read operation;
authorwenzelm
Thu Mar 19 16:56:51 2009 +0100 (2009-03-19)
changeset 305901d9c9fcf8513
parent 30589 cbe27c4ef417
child 30591 6c9c00ea4ae6
parameterized datatype antiquote and read operation;
src/Pure/General/antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Thu Mar 19 15:44:14 2009 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Thu Mar 19 16:56:51 2009 +0100
     1.3 @@ -6,11 +6,16 @@
     1.4  
     1.5  signature ANTIQUOTE =
     1.6  sig
     1.7 -  datatype antiquote =
     1.8 -    Text of Symbol_Pos.T list | Antiq of Symbol_Pos.T list * Position.T |
     1.9 -    Open of Position.T | Close of Position.T
    1.10 -  val is_antiq: antiquote -> bool
    1.11 -  val read: Symbol_Pos.T list * Position.T -> antiquote list
    1.12 +  datatype 'a antiquote =
    1.13 +    Text of 'a |
    1.14 +    Antiq of Symbol_Pos.T list * Position.T |
    1.15 +    Open of Position.T |
    1.16 +    Close of Position.T
    1.17 +  val is_antiq: 'a antiquote -> bool
    1.18 +  val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
    1.19 +  val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
    1.20 +  val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
    1.21 +    Symbol_Pos.T list * Position.T -> 'a antiquote list
    1.22  end;
    1.23  
    1.24  structure Antiquote: ANTIQUOTE =
    1.25 @@ -18,8 +23,8 @@
    1.26  
    1.27  (* datatype antiquote *)
    1.28  
    1.29 -datatype antiquote =
    1.30 -  Text of Symbol_Pos.T list |
    1.31 +datatype 'a antiquote =
    1.32 +  Text of 'a |
    1.33    Antiq of Symbol_Pos.T list * Position.T |
    1.34    Open of Position.T |
    1.35    Close of Position.T;
    1.36 @@ -44,7 +49,7 @@
    1.37    in check antiqs [] end;
    1.38  
    1.39  
    1.40 -(* scan_antiquote *)
    1.41 +(* scan *)
    1.42  
    1.43  open Basic_Symbol_Pos;
    1.44  
    1.45 @@ -63,15 +68,15 @@
    1.46    Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    1.47      Symbol_Pos.!!! "missing closing brace of antiquotation"
    1.48        (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    1.49 -  >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
    1.50 +  >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
    1.51 +
    1.52 +val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
    1.53 +val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
    1.54  
    1.55  in
    1.56  
    1.57 -val scan_antiquote =
    1.58 - (Scan.repeat1 scan_txt >> (Text o flat) ||
    1.59 -  scan_antiq ||
    1.60 -  Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
    1.61 -  Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
    1.62 +fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
    1.63 +val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
    1.64  
    1.65  end;
    1.66  
    1.67 @@ -81,9 +86,9 @@
    1.68  fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
    1.69    | report_antiq _ = ();
    1.70  
    1.71 -fun read ([], _) = []
    1.72 -  | read (syms, pos) =
    1.73 -      (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
    1.74 +fun read _ ([], _) = []
    1.75 +  | read scanner (syms, pos) =
    1.76 +      (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
    1.77          SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
    1.78        | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    1.79  
     2.1 --- a/src/Pure/ML/ml_context.ML	Thu Mar 19 15:44:14 2009 +0100
     2.2 +++ b/src/Pure/ML/ml_context.ML	Thu Mar 19 16:56:51 2009 +0100
     2.3 @@ -194,7 +194,7 @@
     2.4  fun eval_antiquotes (txt, pos) opt_context =
     2.5    let
     2.6      val syms = Symbol_Pos.explode (txt, pos);
     2.7 -    val ants = Antiquote.read (syms, pos);
     2.8 +    val ants = Antiquote.read Antiquote.scan_text (syms, pos);
     2.9      val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
    2.10      val ((ml_env, ml_body), opt_ctxt') =
    2.11        if not (exists Antiquote.is_antiq ants)
     3.1 --- a/src/Pure/Thy/latex.ML	Thu Mar 19 15:44:14 2009 +0100
     3.2 +++ b/src/Pure/Thy/latex.ML	Thu Mar 19 16:56:51 2009 +0100
     3.3 @@ -117,7 +117,7 @@
     3.4      else if T.is_kind T.Verbatim tok then
     3.5        let
     3.6          val (txt, pos) = T.source_position_of tok;
     3.7 -        val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
     3.8 +        val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
     3.9          val out = implode (map output_syms_antiq ants);
    3.10        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    3.11      else output_syms s
     4.1 --- a/src/Pure/Thy/thy_output.ML	Thu Mar 19 15:44:14 2009 +0100
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Mar 19 16:56:51 2009 +0100
     4.3 @@ -156,7 +156,7 @@
     4.4            end
     4.5        | expand (Antiquote.Open _) = ""
     4.6        | expand (Antiquote.Close _) = "";
     4.7 -    val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
     4.8 +    val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
     4.9    in
    4.10      if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
    4.11        error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)