optional description for 'attribute_setup' and 'method_setup';
authorwenzelm
Sun May 15 17:06:35 2011 +0200 (2011-05-15)
changeset 428136c841fa92fa2
parent 42812 dda4aef7cba4
child 42814 5af15f1e2ef6
optional description for 'attribute_setup' and 'method_setup';
doc-src/IsarRef/Thy/Proof.thy
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/document/Proof.tex
doc-src/IsarRef/Thy/document/Spec.tex
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/method.ML
     1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Sun May 15 16:40:24 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Sun May 15 17:06:35 2011 +0200
     1.3 @@ -896,7 +896,7 @@
     1.4    \end{matharray}
     1.5  
     1.6    @{rail "
     1.7 -    @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}
     1.8 +    @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
     1.9      ;
    1.10    "}
    1.11  
     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sun May 15 16:40:24 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Sun May 15 17:06:35 2011 +0200
     2.3 @@ -859,7 +859,7 @@
     2.4      (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
     2.5        @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
     2.6      ;
     2.7 -    @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}
     2.8 +    @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
     2.9    "}
    2.10  
    2.11    \begin{description}
     3.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Sun May 15 16:40:24 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Sun May 15 17:06:35 2011 +0200
     3.3 @@ -1234,12 +1234,15 @@
     3.4    \end{matharray}
     3.5  
     3.6    \begin{railoutput}
     3.7 -\rail@begin{1}{}
     3.8 +\rail@begin{2}{}
     3.9  \rail@term{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
    3.10  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    3.11  \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
    3.12  \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
    3.13 +\rail@bar
    3.14 +\rail@nextbar{1}
    3.15  \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
    3.16 +\rail@endbar
    3.17  \rail@end
    3.18  \end{railoutput}
    3.19  
     4.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun May 15 16:40:24 2011 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun May 15 17:06:35 2011 +0200
     4.3 @@ -1280,12 +1280,15 @@
     4.4  \rail@endbar
     4.5  \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
     4.6  \rail@end
     4.7 -\rail@begin{1}{}
     4.8 +\rail@begin{2}{}
     4.9  \rail@term{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
    4.10  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    4.11  \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
    4.12  \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
    4.13 +\rail@bar
    4.14 +\rail@nextbar{1}
    4.15  \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
    4.16 +\rail@endbar
    4.17  \rail@end
    4.18  \end{railoutput}
    4.19  
     5.1 --- a/src/Pure/Isar/attrib.ML	Sun May 15 16:40:24 2011 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Sun May 15 17:06:35 2011 +0200
     5.3 @@ -78,8 +78,9 @@
     5.4    let
     5.5      val ctxt = Proof_Context.init_global thy;
     5.6      val attribs = Attributes.get thy;
     5.7 -    fun prt_attr (name, (_, comment)) = Pretty.block
     5.8 -      [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     5.9 +    fun prt_attr (name, (_, "")) = Pretty.str name
    5.10 +      | prt_attr (name, (_, comment)) =
    5.11 +          Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    5.12    in
    5.13      [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
    5.14      |> Pretty.chunks |> Pretty.writeln
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Sun May 15 16:40:24 2011 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun May 15 17:06:35 2011 +0200
     6.3 @@ -327,12 +327,14 @@
     6.4  
     6.5  val _ =
     6.6    Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
     6.7 -    (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
     6.8 +    (Parse.position Parse.name --
     6.9 +        Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
    6.10        >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
    6.11  
    6.12  val _ =
    6.13    Outer_Syntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
    6.14 -    (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
    6.15 +    (Parse.position Parse.name --
    6.16 +        Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
    6.17        >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
    6.18  
    6.19  val _ =
     7.1 --- a/src/Pure/Isar/method.ML	Sun May 15 16:40:24 2011 +0200
     7.2 +++ b/src/Pure/Isar/method.ML	Sun May 15 17:06:35 2011 +0200
     7.3 @@ -336,8 +336,9 @@
     7.4    let
     7.5      val ctxt = Proof_Context.init_global thy;
     7.6      val meths = Methods.get thy;
     7.7 -    fun prt_meth (name, (_, comment)) = Pretty.block
     7.8 -      [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     7.9 +    fun prt_meth (name, (_, "")) = Pretty.str name
    7.10 +      | prt_meth (name, (_, comment)) =
    7.11 +          Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    7.12    in
    7.13      [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table ctxt meths))]
    7.14      |> Pretty.chunks |> Pretty.writeln