src/Pure/Isar/antiquote.ML
author wenzelm
Tue Feb 12 20:34:02 2002 +0100 (2002-02-12)
changeset 12881 eeb36b66480e
parent 9138 6a4fae41a75f
child 14598 7009f59711e3
permissions -rw-r--r--
ANTIQUOTE_FAIL;
wenzelm@9138
     1
(*  Title:      Pure/Isar/antiquote.ML
wenzelm@9138
     2
    ID:         $Id$
wenzelm@9138
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9138
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@9138
     5
wenzelm@9138
     6
Text with antiquotations of inner items (terms, types etc.).
wenzelm@9138
     7
*)
wenzelm@9138
     8
wenzelm@9138
     9
signature ANTIQUOTE =
wenzelm@9138
    10
sig
wenzelm@12881
    11
  exception ANTIQUOTE_FAIL of (string * Position.T) * exn
wenzelm@9138
    12
  datatype antiquote = Text of string | Antiq of string * Position.T
wenzelm@9138
    13
  val is_antiq: antiquote -> bool
wenzelm@9138
    14
  val antiquotes_of: string * Position.T -> antiquote list
wenzelm@9138
    15
end;
wenzelm@9138
    16
wenzelm@9138
    17
structure Antiquote: ANTIQUOTE =
wenzelm@9138
    18
struct
wenzelm@9138
    19
wenzelm@9138
    20
(* datatype antiquote *)
wenzelm@9138
    21
wenzelm@12881
    22
exception ANTIQUOTE_FAIL of (string * Position.T) * exn;
wenzelm@12881
    23
wenzelm@9138
    24
datatype antiquote =
wenzelm@9138
    25
  Text of string |
wenzelm@9138
    26
  Antiq of string * Position.T;
wenzelm@9138
    27
wenzelm@9138
    28
fun is_antiq (Text _) = false
wenzelm@9138
    29
  | is_antiq (Antiq _) = true;
wenzelm@9138
    30
wenzelm@9138
    31
wenzelm@9138
    32
(* scan_antiquote *)
wenzelm@9138
    33
wenzelm@9138
    34
local
wenzelm@9138
    35
wenzelm@9138
    36
structure T = OuterLex;
wenzelm@9138
    37
wenzelm@9138
    38
val scan_txt =
wenzelm@9138
    39
  T.scan_blank ||
wenzelm@9138
    40
  T.keep_line ($$ "@" --| Scan.ahead (Scan.one (not_equal "{"))) ||
wenzelm@9138
    41
  T.keep_line (Scan.one (not_equal "@" andf Symbol.not_sync andf Symbol.not_eof));
wenzelm@9138
    42
wenzelm@9138
    43
fun escape "\\" = "\\\\"
wenzelm@9138
    44
  | escape "\"" = "\\\""
wenzelm@9138
    45
  | escape s = s;
wenzelm@9138
    46
wenzelm@9138
    47
val quote_escape = quote o implode o map escape o Symbol.explode;
wenzelm@9138
    48
wenzelm@9138
    49
val scan_ant =
wenzelm@9138
    50
  T.scan_blank ||
wenzelm@9138
    51
  T.scan_string >> quote_escape ||
wenzelm@9138
    52
  T.keep_line (Scan.one (not_equal "}" andf Symbol.not_sync andf Symbol.not_eof));
wenzelm@9138
    53
wenzelm@9138
    54
val scan_antiq =
wenzelm@9138
    55
  T.keep_line ($$ "@" -- $$ "{") |--
wenzelm@9138
    56
    T.!!! "missing closing brace of antiquotation"
wenzelm@9138
    57
      (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
wenzelm@9138
    58
wenzelm@9138
    59
in
wenzelm@9138
    60
wenzelm@9138
    61
fun scan_antiquote (pos, ss) = (pos, ss) |>
wenzelm@9138
    62
  (Scan.repeat1 scan_txt >> (Text o implode) ||
wenzelm@9138
    63
    scan_antiq >> (fn s => Antiq (s, pos)));
wenzelm@9138
    64
wenzelm@9138
    65
end;
wenzelm@9138
    66
wenzelm@9138
    67
wenzelm@9138
    68
(* antiquotes_of *)
wenzelm@9138
    69
wenzelm@9138
    70
fun antiquotes_of (s, pos) =
wenzelm@9138
    71
  (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
wenzelm@9138
    72
      (pos, Symbol.explode s) of
wenzelm@9138
    73
    (xs, (_, [])) => xs
wenzelm@9138
    74
  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation text at: " ^
wenzelm@9138
    75
      quote (Symbol.beginning ss) ^ Position.str_of pos'));
wenzelm@9138
    76
wenzelm@9138
    77
wenzelm@9138
    78
end;