src/Pure/ProofGeneral/pgip_parser.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32466 a393b7e2a2f8
child 33038 8f9594c31de4
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
wenzelm@23797
     1
(*  Title:      Pure/ProofGeneral/pgip_parser.ML
wenzelm@23797
     2
    Author:     David Aspinall and Makarius
wenzelm@23797
     3
wenzelm@23797
     4
Parsing theory sources without execution (via keyword classification).
wenzelm@23797
     5
*)
wenzelm@23797
     6
wenzelm@23797
     7
signature PGIP_PARSER =
wenzelm@23797
     8
sig
wenzelm@23797
     9
  val pgip_parser: Position.T -> string -> PgipMarkup.pgipdocument
wenzelm@23797
    10
end
wenzelm@23797
    11
wenzelm@23797
    12
structure PgipParser: PGIP_PARSER =
wenzelm@23797
    13
struct
wenzelm@23797
    14
wenzelm@23797
    15
structure K = OuterKeyword;
wenzelm@23797
    16
structure D = PgipMarkup;
wenzelm@23797
    17
structure I = PgipIsabelle;
wenzelm@23797
    18
wenzelm@23797
    19
wenzelm@23797
    20
fun badcmd text = [D.Badcmd {text = text}];
wenzelm@23797
    21
wenzelm@23797
    22
fun thy_begin text =
wenzelm@32466
    23
  (case try (Thy_Header.read Position.none) (Source.of_string text) of
aspinall@24192
    24
    NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
wenzelm@23797
    25
  | SOME (name, imports, _) =>
aspinall@24192
    26
       D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
aspinall@24192
    27
  :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
wenzelm@23797
    28
wenzelm@23797
    29
fun thy_heading text =
wenzelm@23797
    30
  [D.Closeblock {},
wenzelm@23797
    31
   D.Doccomment {text = text},
wenzelm@23797
    32
   D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
wenzelm@23797
    33
wenzelm@23797
    34
fun thy_decl text =
wenzelm@23797
    35
  [D.Theoryitem {name = NONE, objtype = SOME I.ObjTheoryDecl, text = text}];
wenzelm@23797
    36
wenzelm@23797
    37
fun goal text =
wenzelm@23797
    38
  [D.Opengoal {thmname = NONE, text = text},
wenzelm@23797
    39
   D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
wenzelm@23797
    40
wenzelm@23797
    41
fun prf_block text =
wenzelm@23797
    42
  [D.Closeblock {},
wenzelm@23797
    43
   D.Proofstep {text = text},
wenzelm@23797
    44
   D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
wenzelm@23797
    45
wenzelm@23797
    46
fun prf_open text =
wenzelm@23797
    47
 [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody},
wenzelm@23797
    48
  D.Proofstep {text = text}];
wenzelm@23797
    49
wenzelm@23797
    50
fun proofstep text = [D.Proofstep {text = text}];
wenzelm@23797
    51
fun closegoal text = [D.Closegoal {text = text}, D.Closeblock {}];
wenzelm@23797
    52
wenzelm@23797
    53
wenzelm@23797
    54
fun command k f = Symtab.update_new (OuterKeyword.kind_of k, f);
wenzelm@23797
    55
wenzelm@23797
    56
val command_keywords = Symtab.empty
wenzelm@23797
    57
  |> command K.control          badcmd
wenzelm@23797
    58
  |> command K.diag             (fn text => [D.Spuriouscmd {text = text}])
wenzelm@23797
    59
  |> command K.thy_begin        thy_begin
wenzelm@23797
    60
  |> command K.thy_switch       badcmd
wenzelm@23797
    61
  |> command K.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
wenzelm@23797
    62
  |> command K.thy_heading      thy_heading
wenzelm@23797
    63
  |> command K.thy_decl         thy_decl
wenzelm@23797
    64
  |> command K.thy_script       thy_decl
wenzelm@23797
    65
  |> command K.thy_goal         goal
wenzelm@23797
    66
  |> command K.qed              closegoal
wenzelm@23797
    67
  |> command K.qed_block        closegoal
wenzelm@23797
    68
  |> command K.qed_global       (fn text => [D.Giveupgoal {text = text}])
wenzelm@23797
    69
  |> command K.prf_heading      (fn text => [D.Doccomment {text = text}])
wenzelm@23797
    70
  |> command K.prf_goal         goal
wenzelm@23797
    71
  |> command K.prf_block        prf_block
wenzelm@23797
    72
  |> command K.prf_open         prf_open
wenzelm@23797
    73
  |> command K.prf_close        (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
wenzelm@23797
    74
  |> command K.prf_chain        proofstep
wenzelm@23797
    75
  |> command K.prf_decl         proofstep
wenzelm@23797
    76
  |> command K.prf_asm          proofstep
wenzelm@23797
    77
  |> command K.prf_asm_goal     goal
wenzelm@23797
    78
  |> command K.prf_script       proofstep;
wenzelm@23797
    79
haftmann@33037
    80
val _ = gen_subset (op =) (OuterKeyword.kinds, Symtab.keys command_keywords)
wenzelm@23797
    81
  orelse sys_error "Incomplete coverage of command keywords";
wenzelm@23797
    82
wenzelm@23797
    83
fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
wenzelm@23797
    84
  | parse_command name text =
wenzelm@27353
    85
      (case OuterKeyword.command_keyword name of
wenzelm@23797
    86
        NONE => [D.Unparseable {text = text}]
wenzelm@23797
    87
      | SOME k =>
wenzelm@23797
    88
          (case Symtab.lookup command_keywords (OuterKeyword.kind_of k) of
wenzelm@23797
    89
            NONE => [D.Unparseable {text = text}]
wenzelm@23797
    90
          | SOME f => f text));
wenzelm@23797
    91
wenzelm@27841
    92
fun parse_span span =
wenzelm@27841
    93
  let
wenzelm@29315
    94
    val kind = ThySyntax.span_kind span;
wenzelm@29315
    95
    val toks = ThySyntax.span_content span;
wenzelm@29315
    96
    val text = implode (map (PrintMode.setmp [] ThySyntax.present_token) toks);
wenzelm@27841
    97
  in
wenzelm@23797
    98
    (case kind of
wenzelm@29315
    99
      ThySyntax.Command name => parse_command name text
wenzelm@29315
   100
    | ThySyntax.Ignored => [D.Whitespace {text = text}]
wenzelm@29315
   101
    | ThySyntax.Malformed => [D.Unparseable {text = text}])
wenzelm@23797
   102
  end;
wenzelm@23797
   103
wenzelm@23797
   104
wenzelm@23797
   105
fun pgip_parser pos str =
wenzelm@29315
   106
  maps parse_span (ThySyntax.parse_spans (OuterKeyword.get_lexicons ()) pos str);
wenzelm@23797
   107
wenzelm@23797
   108
end;