src/Pure/ProofGeneral/pgip_parser.ML
author wenzelm
Fri Jun 13 21:04:42 2008 +0200 (2008-06-13)
changeset 27195 bbf4cbc69243
parent 24192 4eccd4bb8b64
child 27353 71c4dd53d4cb
permissions -rw-r--r--
map_const: soft version, no failure here;
     1 (*  Title:      Pure/ProofGeneral/pgip_parser.ML
     2     ID:         $Id$
     3     Author:     David Aspinall and Makarius
     4 
     5 Parsing theory sources without execution (via keyword classification).
     6 *)
     7 
     8 signature PGIP_PARSER =
     9 sig
    10   val pgip_parser: Position.T -> string -> PgipMarkup.pgipdocument
    11 end
    12 
    13 structure PgipParser: PGIP_PARSER =
    14 struct
    15 
    16 structure K = OuterKeyword;
    17 structure D = PgipMarkup;
    18 structure I = PgipIsabelle;
    19 
    20 
    21 fun badcmd text = [D.Badcmd {text = text}];
    22 
    23 fun thy_begin text =
    24   (case try (ThyHeader.read Position.none) (Source.of_string text) of
    25     NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
    26   | SOME (name, imports, _) =>
    27        D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
    28   :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
    29 
    30 fun thy_heading text =
    31   [D.Closeblock {},
    32    D.Doccomment {text = text},
    33    D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
    34 
    35 fun thy_decl text =
    36   [D.Theoryitem {name = NONE, objtype = SOME I.ObjTheoryDecl, text = text}];
    37 
    38 fun goal text =
    39   [D.Opengoal {thmname = NONE, text = text},
    40    D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
    41 
    42 fun prf_block text =
    43   [D.Closeblock {},
    44    D.Proofstep {text = text},
    45    D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
    46 
    47 fun prf_open text =
    48  [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody},
    49   D.Proofstep {text = text}];
    50 
    51 fun proofstep text = [D.Proofstep {text = text}];
    52 fun closegoal text = [D.Closegoal {text = text}, D.Closeblock {}];
    53 
    54 
    55 fun command k f = Symtab.update_new (OuterKeyword.kind_of k, f);
    56 
    57 val command_keywords = Symtab.empty
    58   |> command K.control          badcmd
    59   |> command K.diag             (fn text => [D.Spuriouscmd {text = text}])
    60   |> command K.thy_begin        thy_begin
    61   |> command K.thy_switch       badcmd
    62   |> command K.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
    63   |> command K.thy_heading      thy_heading
    64   |> command K.thy_decl         thy_decl
    65   |> command K.thy_script       thy_decl
    66   |> command K.thy_goal         goal
    67   |> command K.qed              closegoal
    68   |> command K.qed_block        closegoal
    69   |> command K.qed_global       (fn text => [D.Giveupgoal {text = text}])
    70   |> command K.prf_heading      (fn text => [D.Doccomment {text = text}])
    71   |> command K.prf_goal         goal
    72   |> command K.prf_block        prf_block
    73   |> command K.prf_open         prf_open
    74   |> command K.prf_close        (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
    75   |> command K.prf_chain        proofstep
    76   |> command K.prf_decl         proofstep
    77   |> command K.prf_asm          proofstep
    78   |> command K.prf_asm_goal     goal
    79   |> command K.prf_script       proofstep;
    80 
    81 val _ = OuterKeyword.kinds subset_string Symtab.keys command_keywords
    82   orelse sys_error "Incomplete coverage of command keywords";
    83 
    84 fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
    85   | parse_command name text =
    86       (case OuterSyntax.command_keyword name of
    87         NONE => [D.Unparseable {text = text}]
    88       | SOME k =>
    89           (case Symtab.lookup command_keywords (OuterKeyword.kind_of k) of
    90             NONE => [D.Unparseable {text = text}]
    91           | SOME f => f text));
    92 
    93 fun parse_item (kind, toks) =
    94   let val text = implode (map (PgmlIsabelle.pgml_mode ThyEdit.present_token) toks) in
    95     (case kind of
    96       ThyEdit.Whitespace => [D.Whitespace {text = text}]
    97     | ThyEdit.Junk => [D.Unparseable {text = text}]
    98     | ThyEdit.Commandspan name => parse_command name text)
    99   end;
   100 
   101 
   102 fun pgip_parser pos str =
   103   maps parse_item (ThyEdit.parse_items pos (Source.of_string str));
   104 
   105 end;