src/Pure/Thy/thy_syntax.ML
author wenzelm
Mon, 29 Aug 2011 21:55:49 +0200
changeset 44574 24444588fddd
parent 44354 88bf93c2ae7c
child 44658 5bec9c15ef29
permissions -rw-r--r--
actual auto loading of required files; eliminated File_Store in favour of Thy_Load; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29315
b074c05f00ad renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents: 28454
diff changeset
     1
(*  Title:      Pure/Thy/thy_syntax.ML
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
     3
29315
b074c05f00ad renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents: 28454
diff changeset
     4
Superficial theory syntax: tokens and spans.
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
     5
*)
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
     6
29315
b074c05f00ad renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents: 28454
diff changeset
     7
signature THY_SYNTAX =
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
     8
sig
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
     9
  val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    10
    (Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
27770
10d84e124a2f updated type of nested sources;
wenzelm
parents: 27756
diff changeset
    11
      Source.source) Source.source) Source.source) Source.source
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    12
  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
40131
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 39507
diff changeset
    13
  val present_token: Token.T -> Output.output
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    14
  val report_token: Token.T -> unit
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
    15
  datatype span_kind = Command of string | Ignored | Malformed
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
    16
  type span
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
    17
  val span_kind: span -> span_kind
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    18
  val span_content: span -> Token.T list
27665
b9e54ba563b3 renamed item to span, renamed contructors;
wenzelm
parents: 27353
diff changeset
    19
  val span_range: span -> Position.range
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    20
  val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
    21
  val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
40131
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 39507
diff changeset
    22
  val present_span: span -> Output.output
43621
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
    23
  type element = {head: span, proof: span list, proper_proof: bool}
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
    24
  val element_source: (span, 'a) Source.source ->
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
    25
    (element, (span, 'a) Source.source) Source.source
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    26
end;
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    27
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37197
diff changeset
    28
structure Thy_Syntax: THY_SYNTAX =
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    29
struct
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    30
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
    31
(** tokens **)
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
    32
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
    33
(* parse *)
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    34
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 40290
diff changeset
    35
fun token_source lexs pos =
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 40290
diff changeset
    36
  Symbol.source #> Token.source {do_recover = SOME false} (K lexs) pos;
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    37
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 40290
diff changeset
    38
fun parse_tokens lexs pos =
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 40290
diff changeset
    39
  Source.of_string #> token_source lexs pos #> Source.exhaust;
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    40
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    41
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
    42
(* present *)
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    43
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    44
local
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    45
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    46
val token_kind_markup =
37193
a4b2bb0dab08 simplified command/keyword markup;
wenzelm
parents: 37192
diff changeset
    47
 fn Token.Command       => Markup.command
a4b2bb0dab08 simplified command/keyword markup;
wenzelm
parents: 37192
diff changeset
    48
  | Token.Keyword       => Markup.keyword
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    49
  | Token.Ident         => Markup.ident
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    50
  | Token.LongIdent     => Markup.ident
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    51
  | Token.SymIdent      => Markup.ident
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    52
  | Token.Var           => Markup.var
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    53
  | Token.TypeIdent     => Markup.tfree
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    54
  | Token.TypeVar       => Markup.tvar
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    55
  | Token.Nat           => Markup.ident
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 40131
diff changeset
    56
  | Token.Float         => Markup.ident
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    57
  | Token.String        => Markup.string
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    58
  | Token.AltString     => Markup.altstring
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    59
  | Token.Verbatim      => Markup.verbatim
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38471
diff changeset
    60
  | Token.Space         => Markup.empty
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    61
  | Token.Comment       => Markup.comment
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38471
diff changeset
    62
  | Token.InternalValue => Markup.empty
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    63
  | Token.Error _       => Markup.malformed
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    64
  | Token.Sync          => Markup.control
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    65
  | Token.EOF           => Markup.control;
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    66
37192
8cdddd689ea9 markup non-identifier keyword as operator;
wenzelm
parents: 36959
diff changeset
    67
fun token_markup tok =
43430
1ed88ddf1268 more uniform treatment of "keyword" vs. "operator";
wenzelm
parents: 42290
diff changeset
    68
  if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok then Markup.operator
37197
953fc4983439 more detailed token markup, including command kind as sub_kind;
wenzelm
parents: 37193
diff changeset
    69
  else
953fc4983439 more detailed token markup, including command kind as sub_kind;
wenzelm
parents: 37193
diff changeset
    70
    let
953fc4983439 more detailed token markup, including command kind as sub_kind;
wenzelm
parents: 37193
diff changeset
    71
      val kind = Token.kind_of tok;
953fc4983439 more detailed token markup, including command kind as sub_kind;
wenzelm
parents: 37193
diff changeset
    72
      val props =
38471
0924654b8163 report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;
wenzelm
parents: 38422
diff changeset
    73
        if kind = Token.Command
0924654b8163 report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;
wenzelm
parents: 38422
diff changeset
    74
        then Markup.properties [(Markup.nameN, Token.content_of tok)]
37197
953fc4983439 more detailed token markup, including command kind as sub_kind;
wenzelm
parents: 37193
diff changeset
    75
        else I;
953fc4983439 more detailed token markup, including command kind as sub_kind;
wenzelm
parents: 37193
diff changeset
    76
    in props (token_kind_markup kind) end;
37192
8cdddd689ea9 markup non-identifier keyword as operator;
wenzelm
parents: 36959
diff changeset
    77
40528
d5e9f7608341 report malformed symbols;
wenzelm
parents: 40523
diff changeset
    78
fun report_symbol (sym, pos) =
d5e9f7608341 report malformed symbols;
wenzelm
parents: 40523
diff changeset
    79
  if Symbol.is_malformed sym then Position.report pos Markup.malformed else ();
d5e9f7608341 report malformed symbols;
wenzelm
parents: 40523
diff changeset
    80
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
    81
in
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
    82
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    83
fun present_token tok =
37192
8cdddd689ea9 markup non-identifier keyword as operator;
wenzelm
parents: 36959
diff changeset
    84
  Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
    85
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
    86
fun report_token tok =
40528
d5e9f7608341 report malformed symbols;
wenzelm
parents: 40523
diff changeset
    87
 (Position.report (Token.position_of tok) (token_markup tok);
d5e9f7608341 report malformed symbols;
wenzelm
parents: 40523
diff changeset
    88
  List.app report_symbol (Symbol_Pos.explode (Token.source_position_of tok)));
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
    89
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
    90
end;
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
    91
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
    92
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
    93
27665
b9e54ba563b3 renamed item to span, renamed contructors;
wenzelm
parents: 27353
diff changeset
    94
(** spans **)
b9e54ba563b3 renamed item to span, renamed contructors;
wenzelm
parents: 27353
diff changeset
    95
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
    96
(* type span *)
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
    97
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
    98
datatype span_kind = Command of string | Ignored | Malformed;
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    99
datatype span = Span of span_kind * Token.T list;
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   100
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   101
fun span_kind (Span (k, _)) = k;
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   102
fun span_content (Span (_, toks)) = toks;
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   103
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   104
fun span_range span =
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   105
  (case span_content span of
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   106
    [] => (Position.none, Position.none)
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   107
  | toks =>
27665
b9e54ba563b3 renamed item to span, renamed contructors;
wenzelm
parents: 27353
diff changeset
   108
      let
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   109
        val start_pos = Token.position_of (hd toks);
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   110
        val end_pos = Token.end_position_of (List.last toks);
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   111
      in (start_pos, end_pos) end);
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   112
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   113
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   114
(* parse *)
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
   115
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   116
local
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   117
44354
wenzelm
parents: 44352
diff changeset
   118
val whitespace = Scan.many (not o Token.is_proper);
wenzelm
parents: 44352
diff changeset
   119
val whitespace1 = Scan.many1 (not o Token.is_proper);
27665
b9e54ba563b3 renamed item to span, renamed contructors;
wenzelm
parents: 27353
diff changeset
   120
44354
wenzelm
parents: 44352
diff changeset
   121
val body = Scan.unless (whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
   122
27665
b9e54ba563b3 renamed item to span, renamed contructors;
wenzelm
parents: 27353
diff changeset
   123
val span =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 30573
diff changeset
   124
  Scan.ahead Parse.command -- Parse.not_eof -- Scan.repeat body
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   125
    >> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
44354
wenzelm
parents: 44352
diff changeset
   126
  whitespace1 >> (fn toks => Span (Ignored, toks)) ||
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   127
  Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
   128
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
   129
in
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
   130
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   131
fun span_source src = Source.source Token.stopper (Scan.bulk span) NONE src;
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   132
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   133
end;
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   134
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   135
fun parse_spans lexs pos str =
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   136
  Source.of_string str
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   137
  |> token_source lexs pos
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   138
  |> span_source
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   139
  |> Source.exhaust;
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   140
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   141
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   142
(* present *)
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   143
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   144
local
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   145
27665
b9e54ba563b3 renamed item to span, renamed contructors;
wenzelm
parents: 27353
diff changeset
   146
fun kind_markup (Command name) = Markup.command_span name
b9e54ba563b3 renamed item to span, renamed contructors;
wenzelm
parents: 27353
diff changeset
   147
  | kind_markup Ignored = Markup.ignored_span
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   148
  | kind_markup Malformed = Markup.malformed_span;
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   149
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   150
in
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   151
27842
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   152
fun present_span span =
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   153
  Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
6c35d50d309f abstract type span, tuned interfaces;
wenzelm
parents: 27770
diff changeset
   154
23803
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   155
end;
11bf7af10ec8 tuned signature;
wenzelm
parents: 23790
diff changeset
   156
28434
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   157
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   158
43621
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   159
(** specification elements: commands with optional proof **)
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   160
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   161
type element = {head: span, proof: span list, proper_proof: bool};
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   162
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   163
fun make_element head proof proper_proof =
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   164
  {head = head, proof = proof, proper_proof = proper_proof};
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   165
28434
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   166
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   167
(* scanning spans *)
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   168
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   169
val eof = Span (Command "", []);
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   170
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   171
fun is_eof (Span (Command "", _)) = true
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   172
  | is_eof _ = false;
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   173
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   174
val not_eof = not o is_eof;
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   175
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   176
val stopper = Scan.stopper (K eof) is_eof;
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   177
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   178
43621
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   179
(* element_source *)
28434
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   180
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   181
local
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   182
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   183
fun command_with pred = Scan.one (fn (Span (Command name, _)) => pred name | _ => false);
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   184
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   185
val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
28454
c63168db774c unit_source: more rigid parsing, stop after final qed;
wenzelm
parents: 28438
diff changeset
   186
  if d <= 0 then Scan.fail
28434
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   187
  else
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 30573
diff changeset
   188
    command_with Keyword.is_qed_global >> pair ~1 ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 30573
diff changeset
   189
    command_with Keyword.is_proof_goal >> pair (d + 1) ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 30573
diff changeset
   190
    (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 30573
diff changeset
   191
    Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
28434
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   192
43621
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   193
val element =
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   194
  command_with Keyword.is_theory_goal -- proof
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   195
    >> (fn (a, (bs, d)) => make_element a bs (d >= 0)) ||
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   196
  Scan.one not_eof >> (fn a => make_element a [] true);
28434
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   197
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   198
in
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   199
43621
e8858190cccd clarified Thy_Syntax.element;
wenzelm
parents: 43430
diff changeset
   200
fun element_source src = Source.source stopper (Scan.bulk element) NONE src;
28434
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   201
23726
2ebecff57b17 Basic editing of theory sources.
wenzelm
parents:
diff changeset
   202
end;
28434
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   203
56f0951f4d26 added unit_source: commands with proof;
wenzelm
parents: 27863
diff changeset
   204
end;