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