# HG changeset patch # User wenzelm # Date 1378202314 -7200 # Node ID 21693b7c8fbf6a2838bae513d660a077b818b4f3 # Parent 1d4a46f1fced93d64fe8da2bf1665e956d0f0777 more liberal 'case' syntax: allow parentheses without arguments; diff -r 1d4a46f1fced -r 21693b7c8fbf src/Doc/IsarRef/Proof.thy --- a/src/Doc/IsarRef/Proof.thy Tue Sep 03 11:55:59 2013 +0200 +++ b/src/Doc/IsarRef/Proof.thy Tue Sep 03 11:58:34 2013 +0200 @@ -1195,7 +1195,7 @@ later. @{rail " - @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) +) ')') + @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')') ; caseref: nameref attributes? ; diff -r 1d4a46f1fced -r 21693b7c8fbf src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Sep 03 11:55:59 2013 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Sep 03 11:58:34 2013 +0200 @@ -608,14 +608,12 @@ (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args))); -val case_spec = - (@{keyword "("} |-- - Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| @{keyword ")"}) || - Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1; - val _ = Outer_Syntax.command @{command_spec "case"} "invoke local context" - (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd))); + ((@{keyword "("} |-- + Parse.!!! (Parse.xname -- Scan.repeat (Parse.maybe Parse.binding) --| @{keyword ")"}) || + Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) => + Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts)))); (* proof structure *)