src/Pure/General/antiquote.ML
author wenzelm
Thu Mar 19 16:56:51 2009 +0100 (2009-03-19)
changeset 30590 1d9c9fcf8513
parent 30589 cbe27c4ef417
child 30613 b22d35d9ef28
permissions -rw-r--r--
parameterized datatype antiquote and read operation;
     1 (*  Title:      Pure/General/antiquote.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Text with antiquotations of inner items (types, terms, theorems etc.).
     5 *)
     6 
     7 signature ANTIQUOTE =
     8 sig
     9   datatype 'a antiquote =
    10     Text of 'a |
    11     Antiq of Symbol_Pos.T list * Position.T |
    12     Open of Position.T |
    13     Close of Position.T
    14   val is_antiq: 'a antiquote -> bool
    15   val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
    16   val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
    17   val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
    18     Symbol_Pos.T list * Position.T -> 'a antiquote list
    19 end;
    20 
    21 structure Antiquote: ANTIQUOTE =
    22 struct
    23 
    24 (* datatype antiquote *)
    25 
    26 datatype 'a antiquote =
    27   Text of 'a |
    28   Antiq of Symbol_Pos.T list * Position.T |
    29   Open of Position.T |
    30   Close of Position.T;
    31 
    32 fun is_antiq (Text _) = false
    33   | is_antiq _ = true;
    34 
    35 
    36 (* check_nesting *)
    37 
    38 fun err_unbalanced pos =
    39   error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
    40 
    41 fun check_nesting antiqs =
    42   let
    43     fun check [] [] = ()
    44       | check [] (pos :: _) = err_unbalanced pos
    45       | check (Open pos :: ants) ps = check ants (pos :: ps)
    46       | check (Close pos :: _) [] = err_unbalanced pos
    47       | check (Close _ :: ants) (_ :: ps) = check ants ps
    48       | check (_ :: ants) ps = check ants ps;
    49   in check antiqs [] end;
    50 
    51 
    52 (* scan *)
    53 
    54 open Basic_Symbol_Pos;
    55 
    56 local
    57 
    58 val scan_txt =
    59   $$$ "@" --| Scan.ahead (~$$$ "{") ||
    60   Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
    61     andalso Symbol.is_regular s) >> single;
    62 
    63 val scan_ant =
    64   Symbol_Pos.scan_quoted ||
    65   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    66 
    67 val scan_antiq =
    68   Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    69     Symbol_Pos.!!! "missing closing brace of antiquotation"
    70       (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    71   >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
    72 
    73 val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
    74 val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
    75 
    76 in
    77 
    78 fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
    79 val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
    80 
    81 end;
    82 
    83 
    84 (* read *)
    85 
    86 fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
    87   | report_antiq _ = ();
    88 
    89 fun read _ ([], _) = []
    90   | read scanner (syms, pos) =
    91       (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
    92         SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
    93       | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    94 
    95 end;