src/Pure/Isar/antiquote.ML
author wenzelm
Tue Jun 24 19:43:18 2008 +0200 (2008-06-24)
changeset 27342 3945da15d410
parent 26002 469ee728a5d7
child 27746 c7aa4c18739d
permissions -rw-r--r--
added Open/Close -- checked blocks;
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@27342
    10
  datatype antiquote =
wenzelm@27342
    11
    Text of string | Antiq of string * Position.T |
wenzelm@27342
    12
    Open of Position.T | Close of Position.T
wenzelm@9138
    13
  val is_antiq: antiquote -> bool
wenzelm@22114
    14
  val scan_antiquotes: string * Position.T -> antiquote list
wenzelm@22114
    15
  val scan_arguments: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
wenzelm@22114
    16
    string * Position.T -> 'a
wenzelm@9138
    17
end;
wenzelm@9138
    18
wenzelm@9138
    19
structure Antiquote: ANTIQUOTE =
wenzelm@9138
    20
struct
wenzelm@9138
    21
wenzelm@9138
    22
(* datatype antiquote *)
wenzelm@9138
    23
wenzelm@9138
    24
datatype antiquote =
wenzelm@9138
    25
  Text of string |
wenzelm@27342
    26
  Antiq of string * Position.T |
wenzelm@27342
    27
  Open of Position.T |
wenzelm@27342
    28
  Close of Position.T;
wenzelm@9138
    29
wenzelm@9138
    30
fun is_antiq (Text _) = false
wenzelm@27342
    31
  | is_antiq _ = true;
wenzelm@27342
    32
wenzelm@27342
    33
wenzelm@27342
    34
(* check_nesting *)
wenzelm@27342
    35
wenzelm@27342
    36
fun err_unbalanced pos =
wenzelm@27342
    37
  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
wenzelm@27342
    38
wenzelm@27342
    39
fun check_nesting antiqs =
wenzelm@27342
    40
  let
wenzelm@27342
    41
    fun check [] [] = ()
wenzelm@27342
    42
      | check [] (pos :: _) = err_unbalanced pos
wenzelm@27342
    43
      | check (Open pos :: ants) ps = check ants (pos :: ps)
wenzelm@27342
    44
      | check (Close pos :: _) [] = err_unbalanced pos
wenzelm@27342
    45
      | check (Close _ :: ants) (_ :: ps) = check ants ps
wenzelm@27342
    46
      | check (_ :: ants) ps = check ants ps;
wenzelm@27342
    47
  in check antiqs [] end;
wenzelm@9138
    48
wenzelm@9138
    49
wenzelm@9138
    50
(* scan_antiquote *)
wenzelm@9138
    51
wenzelm@22114
    52
structure T = OuterLex;
wenzelm@9138
    53
wenzelm@22114
    54
local
wenzelm@9138
    55
wenzelm@9138
    56
val scan_txt =
wenzelm@26002
    57
  T.count ($$ "@" --| Scan.ahead (~$$ "{")) ||
wenzelm@27342
    58
  T.count (Scan.one (fn s =>
wenzelm@27342
    59
    s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>" andalso Symbol.is_regular s));
wenzelm@9138
    60
wenzelm@9138
    61
fun escape "\\" = "\\\\"
wenzelm@9138
    62
  | escape "\"" = "\\\""
wenzelm@9138
    63
  | escape s = s;
wenzelm@9138
    64
berghofe@14598
    65
val quote_escape = Library.quote o implode o map escape o Symbol.explode;
wenzelm@9138
    66
wenzelm@9138
    67
val scan_ant =
wenzelm@9138
    68
  T.scan_string >> quote_escape ||
wenzelm@26002
    69
  T.count (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
wenzelm@9138
    70
wenzelm@9138
    71
val scan_antiq =
wenzelm@26002
    72
  T.count ($$ "@") |-- T.count ($$ "{") |--
wenzelm@9138
    73
    T.!!! "missing closing brace of antiquotation"
wenzelm@26002
    74
      (Scan.repeat scan_ant >> implode) --| T.count ($$ "}");
wenzelm@9138
    75
wenzelm@9138
    76
in
wenzelm@9138
    77
wenzelm@9138
    78
fun scan_antiquote (pos, ss) = (pos, ss) |>
wenzelm@9138
    79
  (Scan.repeat1 scan_txt >> (Text o implode) ||
wenzelm@27342
    80
    scan_antiq >> (fn s => Antiq (s, pos)) ||
wenzelm@27342
    81
    T.count ($$ "\\<lbrace>") >> K (Open pos) ||
wenzelm@27342
    82
    T.count ($$ "\\<rbrace>") >> K (Close pos));
wenzelm@9138
    83
wenzelm@9138
    84
end;
wenzelm@9138
    85
wenzelm@9138
    86
wenzelm@22114
    87
(* scan_antiquotes *)
wenzelm@9138
    88
wenzelm@22114
    89
fun scan_antiquotes (s, pos) =
wenzelm@9138
    90
  (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
wenzelm@9138
    91
      (pos, Symbol.explode s) of
wenzelm@27342
    92
    (xs, (_, [])) => (check_nesting xs; xs)
wenzelm@22114
    93
  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation source at: " ^
wenzelm@14729
    94
      quote (Symbol.beginning 10 ss) ^ Position.str_of pos'));
wenzelm@9138
    95
wenzelm@9138
    96
wenzelm@22114
    97
(* scan_arguments *)
wenzelm@22114
    98
wenzelm@22114
    99
fun scan_arguments lex antiq (s, pos) =
wenzelm@22114
   100
  let
wenzelm@22114
   101
    fun err msg = cat_error msg
wenzelm@22114
   102
      ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
wenzelm@22114
   103
wenzelm@22114
   104
    val res =
wenzelm@22114
   105
      Source.of_string s
wenzelm@22114
   106
      |> Symbol.source false
wenzelm@23677
   107
      |> T.source NONE (K (lex, Scan.empty_lexicon)) pos
wenzelm@22114
   108
      |> T.source_proper
wenzelm@22114
   109
      |> Source.source T.stopper (Scan.error (Scan.bulk antiq)) NONE
wenzelm@22114
   110
      |> Source.exhaust;
wenzelm@22114
   111
  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
wenzelm@22114
   112
wenzelm@9138
   113
end;