# HG changeset patch # User wenzelm # Date 1138881145 -3600 # Node ID e3d2aa8ba0e170b5bd6e58ee86b5481e2980f5ba # Parent b31293969d4fbae392654c123dce5e4d3325429c added parname; added (general_)statement (from isar_syn.ML); general_statement: Elements.statement, i.e. Shows/Obtains; diff -r b31293969d4f -r e3d2aa8ba0e1 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 =