# HG changeset patch
# User wenzelm
# Date 1295186656 -3600
# Node ID 1f930561a560caffd6e3197461e5ee796820ebcc
# Parent  45d7da4e4ccf1f80856a7058baf33d25114de290
more standard command descriptions;

diff -r 45d7da4e4ccf -r 1f930561a560 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Sun Jan 16 14:57:14 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sun Jan 16 15:04:16 2011 +0100
@@ -84,6 +84,7 @@
       ProofContext.init_global |>
       Context.proof_map (fold Element.init context)
   in
+    (* FIXME print as single message, e.g. via Pretty.big_list, Pretty.chunks etc. *)
     (writeln "Context:\n";
      Pretty.chunks (maps (Element.pretty_ctxt ctxt) context) |>
      Pretty.writeln;
@@ -108,7 +109,7 @@
 
 val _ =
   Outer_Syntax.command "spark_open"
-    "Open a new SPARK environment and load a SPARK-generated .vcg or .siv file."
+    "open a new SPARK environment and load a SPARK-generated .vcg or .siv file"
     Keyword.thy_decl
     (Parse.name >> (Toplevel.theory o spark_open));
 
@@ -117,21 +118,21 @@
 
 val _ =
   Outer_Syntax.command "spark_proof_functions"
-    "Associate SPARK proof functions with terms."
+    "associate SPARK proof functions with terms"
     Keyword.thy_decl
     (Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
        (Toplevel.theory o fold add_proof_fun_cmd));
 
 val _ =
   Outer_Syntax.command "spark_vc"
-    "Enter into proof mode for a specific verification condition."
+    "enter into proof mode for a specific verification condition"
     Keyword.thy_goal
     (Parse.name >> (fn name =>
       (Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name))));
 
 val _ =
   Outer_Syntax.improper_command "spark_status"
-    "Show the name and state of all loaded verification conditions."
+    "show the name and state of all loaded verification conditions"
     Keyword.diag
     (Scan.optional
        (Args.parens
@@ -141,7 +142,7 @@
 
 val _ =
   Outer_Syntax.command "spark_end"
-    "Close the current SPARK environment."
+    "close the current SPARK environment"
     Keyword.thy_decl
     (Scan.succeed (Toplevel.theory SPARK_VCs.close));