wenzelm@23797: (*  Title:      Pure/ProofGeneral/pgip_parser.ML
wenzelm@23797:     Author:     David Aspinall and Makarius
wenzelm@23797: 
wenzelm@23797: Parsing theory sources without execution (via keyword classification).
wenzelm@23797: *)
wenzelm@23797: 
wenzelm@23797: signature PGIP_PARSER =
wenzelm@23797: sig
wenzelm@23797:   val pgip_parser: Position.T -> string -> PgipMarkup.pgipdocument
wenzelm@23797: end
wenzelm@23797: 
wenzelm@23797: structure PgipParser: PGIP_PARSER =
wenzelm@23797: struct
wenzelm@23797: 
wenzelm@23797: structure D = PgipMarkup;
wenzelm@23797: structure I = PgipIsabelle;
wenzelm@23797: 
wenzelm@23797: 
wenzelm@23797: fun badcmd text = [D.Badcmd {text = text}];
wenzelm@23797: 
wenzelm@23797: fun thy_begin text =
wenzelm@32466:   (case try (Thy_Header.read Position.none) (Source.of_string text) of
aspinall@24192:     NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
wenzelm@23797:   | SOME (name, imports, _) =>
aspinall@24192:        D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
aspinall@24192:   :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
wenzelm@23797: 
wenzelm@23797: fun thy_heading text =
wenzelm@23797:   [D.Closeblock {},
wenzelm@23797:    D.Doccomment {text = text},
wenzelm@23797:    D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
wenzelm@23797: 
wenzelm@23797: fun thy_decl text =
wenzelm@23797:   [D.Theoryitem {name = NONE, objtype = SOME I.ObjTheoryDecl, text = text}];
wenzelm@23797: 
wenzelm@23797: fun goal text =
wenzelm@23797:   [D.Opengoal {thmname = NONE, text = text},
wenzelm@23797:    D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
wenzelm@23797: 
wenzelm@23797: fun prf_block text =
wenzelm@23797:   [D.Closeblock {},
wenzelm@23797:    D.Proofstep {text = text},
wenzelm@23797:    D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
wenzelm@23797: 
wenzelm@23797: fun prf_open text =
wenzelm@23797:  [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody},
wenzelm@23797:   D.Proofstep {text = text}];
wenzelm@23797: 
wenzelm@23797: fun proofstep text = [D.Proofstep {text = text}];
wenzelm@23797: fun closegoal text = [D.Closegoal {text = text}, D.Closeblock {}];
wenzelm@23797: 
wenzelm@23797: 
wenzelm@36950: fun command k f = Symtab.update_new (Keyword.kind_of k, f);
wenzelm@23797: 
wenzelm@23797: val command_keywords = Symtab.empty
wenzelm@36950:   |> command Keyword.control          badcmd
wenzelm@36950:   |> command Keyword.diag             (fn text => [D.Spuriouscmd {text = text}])
wenzelm@36950:   |> command Keyword.thy_begin        thy_begin
wenzelm@36950:   |> command Keyword.thy_switch       badcmd
wenzelm@36950:   |> command Keyword.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
wenzelm@36950:   |> command Keyword.thy_heading      thy_heading
wenzelm@36950:   |> command Keyword.thy_decl         thy_decl
wenzelm@36950:   |> command Keyword.thy_script       thy_decl
wenzelm@36950:   |> command Keyword.thy_goal         goal
wenzelm@36950:   |> command Keyword.thy_schematic_goal goal
wenzelm@36950:   |> command Keyword.qed              closegoal
wenzelm@36950:   |> command Keyword.qed_block        closegoal
wenzelm@36950:   |> command Keyword.qed_global       (fn text => [D.Giveupgoal {text = text}])
wenzelm@36950:   |> command Keyword.prf_heading      (fn text => [D.Doccomment {text = text}])
wenzelm@36950:   |> command Keyword.prf_goal         goal
wenzelm@36950:   |> command Keyword.prf_block        prf_block
wenzelm@36950:   |> command Keyword.prf_open         prf_open
wenzelm@36950:   |> command Keyword.prf_close        (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
wenzelm@36950:   |> command Keyword.prf_chain        proofstep
wenzelm@36950:   |> command Keyword.prf_decl         proofstep
wenzelm@36950:   |> command Keyword.prf_asm          proofstep
wenzelm@36950:   |> command Keyword.prf_asm_goal     goal
wenzelm@36950:   |> command Keyword.prf_script       proofstep;
wenzelm@23797: 
wenzelm@36950: val _ = subset (op =) (Keyword.kinds, Symtab.keys command_keywords)
wenzelm@23797:   orelse sys_error "Incomplete coverage of command keywords";
wenzelm@23797: 
wenzelm@23797: fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
wenzelm@23797:   | parse_command name text =
wenzelm@36950:       (case Keyword.command_keyword name of
wenzelm@23797:         NONE => [D.Unparseable {text = text}]
wenzelm@23797:       | SOME k =>
wenzelm@36950:           (case Symtab.lookup command_keywords (Keyword.kind_of k) of
wenzelm@23797:             NONE => [D.Unparseable {text = text}]
wenzelm@23797:           | SOME f => f text));
wenzelm@23797: 
wenzelm@27841: fun parse_span span =
wenzelm@27841:   let
wenzelm@29315:     val kind = ThySyntax.span_kind span;
wenzelm@29315:     val toks = ThySyntax.span_content span;
wenzelm@37146:     val text = implode (map (Print_Mode.setmp [] ThySyntax.present_token) toks);
wenzelm@27841:   in
wenzelm@23797:     (case kind of
wenzelm@29315:       ThySyntax.Command name => parse_command name text
wenzelm@29315:     | ThySyntax.Ignored => [D.Whitespace {text = text}]
wenzelm@29315:     | ThySyntax.Malformed => [D.Unparseable {text = text}])
wenzelm@23797:   end;
wenzelm@23797: 
wenzelm@23797: 
wenzelm@23797: fun pgip_parser pos str =
wenzelm@36950:   maps parse_span (ThySyntax.parse_spans (Keyword.get_lexicons ()) pos str);
wenzelm@23797: 
wenzelm@23797: end;