src/Pure/Isar/antiquote.ML
author wenzelm
Mon Jul 09 23:12:44 2007 +0200 (2007-07-09)
changeset 23677 1114cc909800
parent 22114 560c5b5dda1c
child 23784 75e6b9dd5336
permissions -rw-r--r--
adapted OuterLex/T.source;
wenzelm@9138
     1
(*  Title:      Pure/Isar/antiquote.ML
wenzelm@9138
     2
    ID:         $Id$
wenzelm@9138
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9138
     4
wenzelm@9138
     5
Text with antiquotations of inner items (terms, types etc.).
wenzelm@9138
     6
*)
wenzelm@9138
     7
wenzelm@9138
     8
signature ANTIQUOTE =
wenzelm@9138
     9
sig
wenzelm@12881
    10
  exception ANTIQUOTE_FAIL of (string * Position.T) * exn
wenzelm@9138
    11
  datatype antiquote = Text of string | Antiq of string * Position.T
wenzelm@9138
    12
  val is_antiq: antiquote -> bool
wenzelm@22114
    13
  val scan_antiquotes: string * Position.T -> antiquote list
wenzelm@22114
    14
  val scan_arguments: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
wenzelm@22114
    15
    string * Position.T -> 'a
wenzelm@9138
    16
end;
wenzelm@9138
    17
wenzelm@9138
    18
structure Antiquote: ANTIQUOTE =
wenzelm@9138
    19
struct
wenzelm@9138
    20
wenzelm@9138
    21
(* datatype antiquote *)
wenzelm@9138
    22
wenzelm@12881
    23
exception ANTIQUOTE_FAIL of (string * Position.T) * exn;
wenzelm@12881
    24
wenzelm@9138
    25
datatype antiquote =
wenzelm@9138
    26
  Text of string |
wenzelm@9138
    27
  Antiq of string * Position.T;
wenzelm@9138
    28
wenzelm@9138
    29
fun is_antiq (Text _) = false
wenzelm@9138
    30
  | is_antiq (Antiq _) = true;
wenzelm@9138
    31
wenzelm@9138
    32
wenzelm@9138
    33
(* scan_antiquote *)
wenzelm@9138
    34
wenzelm@22114
    35
structure T = OuterLex;
wenzelm@9138
    36
wenzelm@22114
    37
local
wenzelm@9138
    38
wenzelm@9138
    39
val scan_txt =
wenzelm@9138
    40
  T.scan_blank ||
wenzelm@19305
    41
  T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
wenzelm@19305
    42
  T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.not_sync s andalso Symbol.not_eof s));
wenzelm@9138
    43
wenzelm@9138
    44
fun escape "\\" = "\\\\"
wenzelm@9138
    45
  | escape "\"" = "\\\""
wenzelm@9138
    46
  | escape s = s;
wenzelm@9138
    47
berghofe@14598
    48
val quote_escape = Library.quote o implode o map escape o Symbol.explode;
wenzelm@9138
    49
wenzelm@9138
    50
val scan_ant =
wenzelm@9138
    51
  T.scan_blank ||
wenzelm@9138
    52
  T.scan_string >> quote_escape ||
wenzelm@19305
    53
  T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.not_sync s andalso Symbol.not_eof s));
wenzelm@9138
    54
wenzelm@9138
    55
val scan_antiq =
wenzelm@9138
    56
  T.keep_line ($$ "@" -- $$ "{") |--
wenzelm@9138
    57
    T.!!! "missing closing brace of antiquotation"
wenzelm@9138
    58
      (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
wenzelm@9138
    59
wenzelm@9138
    60
in
wenzelm@9138
    61
wenzelm@9138
    62
fun scan_antiquote (pos, ss) = (pos, ss) |>
wenzelm@9138
    63
  (Scan.repeat1 scan_txt >> (Text o implode) ||
wenzelm@9138
    64
    scan_antiq >> (fn s => Antiq (s, pos)));
wenzelm@9138
    65
wenzelm@9138
    66
end;
wenzelm@9138
    67
wenzelm@9138
    68
wenzelm@22114
    69
(* scan_antiquotes *)
wenzelm@9138
    70
wenzelm@22114
    71
fun scan_antiquotes (s, pos) =
wenzelm@9138
    72
  (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
wenzelm@9138
    73
      (pos, Symbol.explode s) of
wenzelm@9138
    74
    (xs, (_, [])) => xs
wenzelm@22114
    75
  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation source at: " ^
wenzelm@14729
    76
      quote (Symbol.beginning 10 ss) ^ Position.str_of pos'));
wenzelm@9138
    77
wenzelm@9138
    78
wenzelm@22114
    79
(* scan_arguments *)
wenzelm@22114
    80
wenzelm@22114
    81
fun scan_arguments lex antiq (s, pos) =
wenzelm@22114
    82
  let
wenzelm@22114
    83
    fun err msg = cat_error msg
wenzelm@22114
    84
      ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
wenzelm@22114
    85
wenzelm@22114
    86
    val res =
wenzelm@22114
    87
      Source.of_string s
wenzelm@22114
    88
      |> Symbol.source false
wenzelm@23677
    89
      |> T.source NONE (K (lex, Scan.empty_lexicon)) pos
wenzelm@22114
    90
      |> T.source_proper
wenzelm@22114
    91
      |> Source.source T.stopper (Scan.error (Scan.bulk antiq)) NONE
wenzelm@22114
    92
      |> Source.exhaust;
wenzelm@22114
    93
  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
wenzelm@22114
    94
wenzelm@9138
    95
end;