src/Pure/Isar/outer_parse.ML

--- a/src/Pure/Isar/outer_parse.ML	Thu Feb 02 12:52:24 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Thu Feb 02 12:52:25 2006 +0100
@@ -50,6 +50,7 @@
   val xname: token list -> xstring * token list
   val text: token list -> string * token list
   val path: token list -> Path.T * token list
+  val parname: token list -> string * token list
   val sort: token list -> string * token list
   val arity: token list -> (string list * string) * token list
   val type_args: token list -> string list * token list
@@ -87,6 +88,11 @@
   val locale_keyword: token list -> string * token list
   val locale_element: token list -> Element.context Locale.element * token list
   val context_element: token list -> Element.context * token list
+  val statement: token list ->
+    ((bstring * Attrib.src list) * (string * (string list * string list)) list) list * token list
+  val general_statement: token list ->
+    (Element.context Locale.element list * Element.statement) * OuterLex.token list
+  val statement_keyword: token list -> string * token list
   val method: token list -> Method.text * token list
 end;
 
@@ -199,6 +205,8 @@
 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
 val path = group "file name/path specification" name >> Path.unpack;
 
+val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
+
 
 (* sorts and arities *)
 
@@ -382,6 +390,23 @@
 end;
 
 
+(* statements *)
+
+val statement = and_list1 (opt_thm_name ":" -- Scan.repeat1 propp);
+
+val obtain_case =
+  parname -- (Scan.optional (simple_fixes --| $$$ "where") [] --
+    (and_list1 (Scan.repeat1 prop) >> List.concat));
+
+val general_statement =
+  statement >> (fn x => ([], Element.Shows x)) ||
+  Scan.repeat locale_element --
+   ($$$ "shows" |-- !!! statement >> Element.Shows ||
+    $$$ "obtains" |-- !!! (enum1 "|" obtain_case) >> Element.Obtains);
+
+val statement_keyword = $$$ "shows" || $$$ "obtains";
+
+
 (* proof methods *)
 
 fun is_symid_meth s =