# HG changeset patch # User aspinall # Date 1167573040 -3600 # Node ID 513e1d82640d26de81baa766f22e6b4d890373e8 # Parent 1845e43aee930c64a0e60e6bd49ef7115f830212 Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command. diff -r 1845e43aee93 -r 513e1d82640d src/Pure/ProofGeneral/parsing.ML --- a/src/Pure/ProofGeneral/parsing.ML Sat Dec 30 16:20:32 2006 +0100 +++ b/src/Pure/ProofGeneral/parsing.ML Sun Dec 31 14:50:40 2006 +0100 @@ -8,6 +8,7 @@ signature PGIP_PARSER = sig val pgip_parser: PgipMarkup.pgip_parser + val init : unit -> unit (* clear state *) end structure PgipParser : PGIP_PARSER = @@ -55,6 +56,26 @@ *) local + val keywords_classification_table = ref (NONE: string Symtab.table option) + +in + fun get_keywords_classification_table () = + case (!keywords_classification_table) of + SOME t => t + | NONE => (let + val tab = fold (fn (c, _, k, _) => Symtab.update (c, k)) + (OuterSyntax.dest_parsers ()) Symtab.empty; + in (keywords_classification_table := SOME tab; tab) end) + + (* To allow dynamic extensions to language during interactive use + we need a hook in outer_syntax.ML to reset our table. But this is + pretty obscure; initialisation at startup should suffice. *) + + fun init () = (keywords_classification_table := NONE) +end + + +local fun whitespace str = D.Whitespace { text=str } @@ -69,21 +90,6 @@ fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg) - (* FIXME: allow dynamic extensions to language here: we need a hook in - outer_syntax.ML to reset this table. *) - - val keywords_classification_table = ref (NONE: string Symtab.table option) - - fun get_keywords_classification_table () = - case (!keywords_classification_table) of - SOME t => t - | NONE => (let - val tab = fold (fn (c, _, k, _) => Symtab.update (c, k)) - (OuterSyntax.dest_parsers ()) Symtab.empty; - in (keywords_classification_table := SOME tab; tab) end) - - - fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *) let val ((thyname,imports,files),_) = ThyHeader.args (toks@sync) @@ -194,8 +200,7 @@ fun xmls_of_kind kind (name,toks,str) = case kind of "control" => [D.Badcmd {text=str}] - | "diag" => [D.Theoryitem {name=NONE,objtype=NONE, - text=str}] (* FIXME: check NOT spuriouscmd *) + | "diag" => [D.Spuriouscmd {text=str}] (* theory/files *) | "theory-begin" => xmls_of_thy_begin (name,toks,str) | "theory-decl" => xmls_of_thy_decl (name,toks,str) @@ -226,7 +231,8 @@ | "qed-block" => xmls_of_qed (name,str) | "qed-global" => xmls_of_qed (name,str) | other => (* default for anything else is "spuriouscmd", ***ignored for undo*** *) - (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other); + (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other ^ + "(treated as spuriouscmd)"); [D.Spuriouscmd {text=str}]) in @@ -235,9 +241,9 @@ val classification = Symtab.lookup (get_keywords_classification_table ()) name in case classification of SOME k => (xmls_of_kind k (name,toks,str)) - | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *) - (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd"); - [D.Spuriouscmd {text=str}]) + | NONE => (* an uncategorized keyword is treated as a theory item (maybe wrong) *) + (parse_warning ("Uncategorized command found: " ^ name ^ " -- using theoryitem"); + [D.Theoryitem {name=NONE,objtype=NONE,text=str}]) end fun markup_comment_whs [] = [] @@ -264,7 +270,7 @@ (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^) -- (spaceP || Scan.succeed "") >> op^ val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync) - (* NB: this collapses litcomment,(litcomment|whitespace)* to a single litcomment *) + (* NB: this collapses doccomment,(doccomment|whitespace)* to a single doccomment *) val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1 val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2 in