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