src/Pure/General/antiquote.ML
author wenzelm
Sat Apr 30 18:16:40 2011 +0200 (2011-04-30)
changeset 42503 27514b6fbe93
parent 39507 839873937ddd
child 42508 e21362bf1d93
permissions -rw-r--r--
more uniform variations of scan_string;
     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.range |
    12     Open of Position.T |
    13     Close of Position.T
    14   val is_text: 'a antiquote -> bool
    15   val report: ('a -> unit) -> 'a antiquote -> unit
    16   val check_nesting: 'a antiquote list -> unit
    17   val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
    18   val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
    19   val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
    20 end;
    21 
    22 structure Antiquote: ANTIQUOTE =
    23 struct
    24 
    25 (* datatype antiquote *)
    26 
    27 datatype 'a antiquote =
    28   Text of 'a |
    29   Antiq of Symbol_Pos.T list * Position.range |
    30   Open of Position.T |
    31   Close of Position.T;
    32 
    33 fun is_text (Text _) = true
    34   | is_text _ = false;
    35 
    36 
    37 (* report *)
    38 
    39 fun report_antiq pos = Position.report pos Markup.antiq;
    40 
    41 fun report report_text (Text x) = report_text x
    42   | report _ (Antiq (_, (pos, _))) = report_antiq pos
    43   | report _ (Open pos) = report_antiq pos
    44   | report _ (Close pos) = report_antiq pos;
    45 
    46 
    47 (* check_nesting *)
    48 
    49 fun err_unbalanced pos =
    50   error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
    51 
    52 fun check_nesting antiqs =
    53   let
    54     fun check [] [] = ()
    55       | check [] (pos :: _) = err_unbalanced pos
    56       | check (Open pos :: ants) ps = check ants (pos :: ps)
    57       | check (Close pos :: _) [] = err_unbalanced pos
    58       | check (Close _ :: ants) (_ :: ps) = check ants ps
    59       | check (_ :: ants) ps = check ants ps;
    60   in check antiqs [] end;
    61 
    62 
    63 (* scan *)
    64 
    65 open Basic_Symbol_Pos;
    66 
    67 local
    68 
    69 val scan_txt =
    70   $$$ "@" --| Scan.ahead (~$$$ "{") ||
    71   Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
    72     andalso Symbol.is_regular s) >> single;
    73 
    74 val scan_ant =
    75   Scan.trace (Symbol_Pos.scan_string_qq || Symbol_Pos.scan_string_bq) >> #2 ||
    76   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    77 
    78 val scan_antiq =
    79   Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    80     Symbol_Pos.!!! "missing closing brace of antiquotation"
    81       (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    82   >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
    83 
    84 val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
    85 val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
    86 
    87 in
    88 
    89 fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
    90 val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
    91 
    92 end;
    93 
    94 
    95 (* read *)
    96 
    97 fun read (syms, pos) =
    98   (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
    99     SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
   100   | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
   101 
   102 end;