src/Pure/Isar/antiquote.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29606 fedb8be05f24
child 30573 49899f26fbd1
permissions -rw-r--r--
use long names for old-style fold combinators;
     1 (*  Title:      Pure/Isar/antiquote.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Text with antiquotations of inner items (terms, types etc.).
     5 *)
     6 
     7 signature ANTIQUOTE =
     8 sig
     9   datatype antiquote =
    10     Text of string | Antiq of SymbolPos.T list * Position.T |
    11     Open of Position.T | Close of Position.T
    12   val is_antiq: antiquote -> bool
    13   val read: SymbolPos.T list * Position.T -> antiquote list
    14   val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
    15     SymbolPos.T list * Position.T -> 'a
    16 end;
    17 
    18 structure Antiquote: ANTIQUOTE =
    19 struct
    20 
    21 (* datatype antiquote *)
    22 
    23 datatype antiquote =
    24   Text of string |
    25   Antiq of SymbolPos.T list * Position.T |
    26   Open of Position.T |
    27   Close of Position.T;
    28 
    29 fun is_antiq (Text _) = false
    30   | is_antiq _ = true;
    31 
    32 
    33 (* check_nesting *)
    34 
    35 fun err_unbalanced pos =
    36   error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
    37 
    38 fun check_nesting antiqs =
    39   let
    40     fun check [] [] = ()
    41       | check [] (pos :: _) = err_unbalanced pos
    42       | check (Open pos :: ants) ps = check ants (pos :: ps)
    43       | check (Close pos :: _) [] = err_unbalanced pos
    44       | check (Close _ :: ants) (_ :: ps) = check ants ps
    45       | check (_ :: ants) ps = check ants ps;
    46   in check antiqs [] end;
    47 
    48 
    49 (* scan_antiquote *)
    50 
    51 open BasicSymbolPos;
    52 structure T = OuterLex;
    53 
    54 local
    55 
    56 val scan_txt =
    57   $$$ "@" --| Scan.ahead (~$$$ "{") ||
    58   Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
    59     andalso Symbol.is_regular s) >> single;
    60 
    61 val scan_ant =
    62   T.scan_quoted ||
    63   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    64 
    65 val scan_antiq =
    66   SymbolPos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    67     T.!!! "missing closing brace of antiquotation"
    68       (Scan.repeat scan_ant -- ($$$ "}" |-- SymbolPos.scan_pos)))
    69   >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
    70 
    71 in
    72 
    73 val scan_antiquote =
    74  (Scan.repeat1 scan_txt >> (Text o SymbolPos.content o flat) ||
    75   scan_antiq ||
    76   SymbolPos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
    77   SymbolPos.scan_pos --| $$$ "\\<rbrace>" >> Close);
    78 
    79 end;
    80 
    81 
    82 (* read *)
    83 
    84 fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
    85   | report_antiq _ = ();
    86 
    87 fun read ([], _) = []
    88   | read (syms, pos) =
    89       (case Scan.read SymbolPos.stopper (Scan.repeat scan_antiquote) syms of
    90         SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
    91       | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    92 
    93 
    94 (* read_antiq *)
    95 
    96 fun read_antiq lex scan (syms, pos) =
    97   let
    98     fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
    99       "@{" ^ SymbolPos.content syms ^ "}");
   100 
   101     val res =
   102       Source.of_list syms
   103       |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
   104       |> T.source_proper
   105       |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE
   106       |> Source.exhaust;
   107   in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
   108 
   109 end;