src/Pure/Thy/thy_syntax.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59125 ee19c92ae8b4
child 59809 87641097d0f3
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm@29315
     1
(*  Title:      Pure/Thy/thy_syntax.ML
wenzelm@23726
     2
    Author:     Makarius
wenzelm@23726
     3
wenzelm@29315
     4
Superficial theory syntax: tokens and spans.
wenzelm@23726
     5
*)
wenzelm@23726
     6
wenzelm@29315
     7
signature THY_SYNTAX =
wenzelm@23726
     8
sig
wenzelm@59123
     9
  val reports_of_tokens: Keyword.keywords -> Token.T list -> bool * Position.report_text list
wenzelm@59123
    10
  val present_token: Keyword.keywords -> Token.T -> Output.output
wenzelm@59123
    11
  val present_span: Keyword.keywords -> Command_Span.span -> Output.output
wenzelm@51225
    12
  datatype 'a element = Element of 'a * ('a element list * 'a) option
wenzelm@51321
    13
  val atom: 'a -> 'a element
wenzelm@51225
    14
  val map_element: ('a -> 'b) -> 'a element -> 'b element
wenzelm@51225
    15
  val flat_element: 'a element -> 'a list
wenzelm@51268
    16
  val last_element: 'a element -> 'a
wenzelm@58923
    17
  val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list
wenzelm@23726
    18
end;
wenzelm@23726
    19
wenzelm@37216
    20
structure Thy_Syntax: THY_SYNTAX =
wenzelm@23726
    21
struct
wenzelm@23726
    22
wenzelm@57905
    23
(** presentation **)
wenzelm@23726
    24
wenzelm@23726
    25
local
wenzelm@23726
    26
wenzelm@59123
    27
fun reports_of_token keywords tok =
wenzelm@48749
    28
  let
wenzelm@48749
    29
    val malformed_symbols =
wenzelm@59064
    30
      Input.source_explode (Token.source_position_of tok)
wenzelm@48749
    31
      |> map_filter (fn (sym, pos) =>
wenzelm@48756
    32
          if Symbol.is_malformed sym
wenzelm@50201
    33
          then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
wenzelm@48749
    34
    val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
wenzelm@59125
    35
    val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
wenzelm@48749
    36
  in (is_malformed, reports) end;
wenzelm@40528
    37
wenzelm@23803
    38
in
wenzelm@23803
    39
wenzelm@59123
    40
fun reports_of_tokens keywords toks =
wenzelm@59123
    41
  let val results = map (reports_of_token keywords) toks
wenzelm@48749
    42
  in (exists fst results, maps snd results) end;
wenzelm@48749
    43
wenzelm@57905
    44
end;
wenzelm@57905
    45
wenzelm@59123
    46
fun present_token keywords tok =
wenzelm@59125
    47
  fold_rev Markup.enclose (Token.markups keywords tok) (Output.output (Token.unparse tok));
wenzelm@23726
    48
wenzelm@59123
    49
fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;
wenzelm@54451
    50
wenzelm@54451
    51
wenzelm@28434
    52
wenzelm@43621
    53
(** specification elements: commands with optional proof **)
wenzelm@43621
    54
wenzelm@51225
    55
datatype 'a element = Element of 'a * ('a element list * 'a) option;
wenzelm@51225
    56
wenzelm@51225
    57
fun element (a, b) = Element (a, SOME b);
wenzelm@51225
    58
fun atom a = Element (a, NONE);
wenzelm@43621
    59
wenzelm@51225
    60
fun map_element f (Element (a, NONE)) = Element (f a, NONE)
wenzelm@51225
    61
  | map_element f (Element (a, SOME (elems, b))) =
wenzelm@51225
    62
      Element (f a, SOME ((map o map_element) f elems, f b));
wenzelm@51225
    63
wenzelm@51225
    64
fun flat_element (Element (a, NONE)) = [a]
wenzelm@51225
    65
  | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
wenzelm@43621
    66
wenzelm@51268
    67
fun last_element (Element (a, NONE)) = a
wenzelm@51268
    68
  | last_element (Element (_, SOME (_, b))) = b;
wenzelm@51268
    69
wenzelm@28434
    70
wenzelm@28434
    71
(* scanning spans *)
wenzelm@28434
    72
wenzelm@57905
    73
val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
wenzelm@28434
    74
wenzelm@57905
    75
fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
wenzelm@28434
    76
  | is_eof _ = false;
wenzelm@28434
    77
wenzelm@28434
    78
val not_eof = not o is_eof;
wenzelm@28434
    79
wenzelm@28434
    80
val stopper = Scan.stopper (K eof) is_eof;
wenzelm@28434
    81
wenzelm@28434
    82
wenzelm@46811
    83
(* parse *)
wenzelm@28434
    84
wenzelm@28434
    85
local
wenzelm@28434
    86
wenzelm@48878
    87
fun command_with pred =
wenzelm@57905
    88
  Scan.one
wenzelm@57905
    89
    (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
wenzelm@28434
    90
wenzelm@58923
    91
fun parse_element keywords =
wenzelm@58923
    92
  let
wenzelm@58923
    93
    val proof_atom =
wenzelm@58923
    94
      Scan.one
wenzelm@58923
    95
        (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
wenzelm@58923
    96
              Keyword.is_proof_body keywords name
wenzelm@58923
    97
          | _ => true) >> atom;
wenzelm@58923
    98
    fun proof_element x =
wenzelm@58923
    99
      (command_with (Keyword.is_proof_goal keywords) -- proof_rest >> element || proof_atom) x
wenzelm@58923
   100
    and proof_rest x =
wenzelm@58923
   101
      (Scan.repeat proof_element -- command_with (Keyword.is_qed keywords)) x;
wenzelm@58923
   102
  in
wenzelm@58923
   103
    command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element ||
wenzelm@58923
   104
    Scan.one not_eof >> atom
wenzelm@58923
   105
  end;
wenzelm@28434
   106
wenzelm@28434
   107
in
wenzelm@28434
   108
wenzelm@58923
   109
fun parse_elements keywords =
wenzelm@46811
   110
  Source.of_list #>
wenzelm@58923
   111
  Source.source stopper (Scan.bulk (parse_element keywords)) #>
wenzelm@46811
   112
  Source.exhaust;
wenzelm@28434
   113
wenzelm@23726
   114
end;
wenzelm@28434
   115
wenzelm@28434
   116
end;