# HG changeset patch
# User wenzelm
# Date 1305471995 -7200
# Node ID 6c841fa92fa2699273ff06db2acb4e9fb94c5c41
# Parent  dda4aef7cba4c6ddb600a165c4277c62a23aa155
optional description for 'attribute_setup' and 'method_setup';

diff -r dda4aef7cba4 -r 6c841fa92fa2 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Sun May 15 16:40:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Sun May 15 17:06:35 2011 +0200
@@ -896,7 +896,7 @@
   \end{matharray}
 
   @{rail "
-    @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}
+    @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
     ;
   "}
 
diff -r dda4aef7cba4 -r 6c841fa92fa2 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Sun May 15 16:40:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sun May 15 17:06:35 2011 +0200
@@ -859,7 +859,7 @@
     (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
       @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
     ;
-    @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}
+    @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
   "}
 
   \begin{description}
diff -r dda4aef7cba4 -r 6c841fa92fa2 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Sun May 15 16:40:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Sun May 15 17:06:35 2011 +0200
@@ -1234,12 +1234,15 @@
   \end{matharray}
 
   \begin{railoutput}
-\rail@begin{1}{}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
+\rail@bar
+\rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
+\rail@endbar
 \rail@end
 \end{railoutput}
 
diff -r dda4aef7cba4 -r 6c841fa92fa2 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun May 15 16:40:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun May 15 17:06:35 2011 +0200
@@ -1280,12 +1280,15 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
 \rail@end
-\rail@begin{1}{}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
+\rail@bar
+\rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
+\rail@endbar
 \rail@end
 \end{railoutput}
 
diff -r dda4aef7cba4 -r 6c841fa92fa2 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun May 15 16:40:24 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun May 15 17:06:35 2011 +0200
@@ -78,8 +78,9 @@
   let
     val ctxt = Proof_Context.init_global thy;
     val attribs = Attributes.get thy;
-    fun prt_attr (name, (_, comment)) = Pretty.block
-      [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
+    fun prt_attr (name, (_, "")) = Pretty.str name
+      | prt_attr (name, (_, comment)) =
+          Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   in
     [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
     |> Pretty.chunks |> Pretty.writeln
diff -r dda4aef7cba4 -r 6c841fa92fa2 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun May 15 16:40:24 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun May 15 17:06:35 2011 +0200
@@ -327,12 +327,14 @@
 
 val _ =
   Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
-    (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
+    (Parse.position Parse.name --
+        Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
 
 val _ =
   Outer_Syntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
-    (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
+    (Parse.position Parse.name --
+        Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
 
 val _ =
diff -r dda4aef7cba4 -r 6c841fa92fa2 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun May 15 16:40:24 2011 +0200
+++ b/src/Pure/Isar/method.ML	Sun May 15 17:06:35 2011 +0200
@@ -336,8 +336,9 @@
   let
     val ctxt = Proof_Context.init_global thy;
     val meths = Methods.get thy;
-    fun prt_meth (name, (_, comment)) = Pretty.block
-      [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
+    fun prt_meth (name, (_, "")) = Pretty.str name
+      | prt_meth (name, (_, comment)) =
+          Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   in
     [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table ctxt meths))]
     |> Pretty.chunks |> Pretty.writeln