refined outer syntax 'help' command;

--- a/NEWS	Mon Nov 26 11:59:56 2012 +0100
+++ b/NEWS	Mon Nov 26 13:54:43 2012 +0100
@@ -41,6 +41,9 @@
 * More informative error messages for Isar proof commands involving
 lazy enumerations (method applications etc.).
 
+* Refined 'help' command to retrieve outer syntax commands according
+to name patterns (with clickable results).
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 

--- a/src/Doc/IsarRef/Misc.thy	Mon Nov 26 11:59:56 2012 +0100
+++ b/src/Doc/IsarRef/Misc.thy	Mon Nov 26 13:54:43 2012 +0100
@@ -8,7 +8,6 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -46,9 +45,6 @@
 
   \begin{description}
   
-  \item @{command "print_commands"} prints Isabelle's outer theory
-  syntax, including keywords and command.
-  
   \item @{command "print_theory"} prints the main logical content of
   the theory context; the ``@{text "!"}'' option indicates extra
   verbosity.

--- a/src/Doc/IsarRef/Outer_Syntax.thy	Mon Nov 26 11:59:56 2012 +0100
+++ b/src/Doc/IsarRef/Outer_Syntax.thy	Mon Nov 26 13:54:43 2012 +0100
@@ -64,6 +64,39 @@
 *}
 
 
+section {* Commands *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+    @{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+  \end{matharray}
+
+  @{rail "
+    @@{command help} (@{syntax name} * )
+  "}
+
+  \begin{description}
+
+  \item @{command "print_commands"} prints all outer syntax keywords
+  and commands.
+
+  \item @{command "help"}~@{text "pats"} retrieves outer syntax
+  commands according to the specified name patterns.
+
+  \end{description}
+*}
+
+
+subsubsection {* Examples *}
+
+text {* Some common diagnostic commands are retrieved like this
+  (according to usual naming conventions): *}
+
+help "print"
+help "find"
+
+
 section {* Lexical matters \label{sec:outer-lex} *}
 
 text {* The outer lexical syntax consists of three main categories of

--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 26 11:59:56 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 26 13:54:43 2012 +0100
@@ -764,8 +764,10 @@
       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "help"} "print outer syntax commands"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
+  Outer_Syntax.improper_command @{command_spec "help"}
+    "retrieve outer syntax commands according to name patterns"
+    (Scan.repeat Parse.name >> (fn pats =>
+      Toplevel.no_timing o Toplevel.imperative (fn () => Outer_Syntax.help_outer_syntax pats)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_commands"} "print outer syntax commands"

--- a/src/Pure/Isar/outer_syntax.ML	Mon Nov 26 11:59:56 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Nov 26 13:54:43 2012 +0100
@@ -28,6 +28,7 @@
     (bool -> local_theory -> Proof.state) parser -> unit
   val local_theory_to_proof: command_spec -> string ->
     (local_theory -> Proof.state) parser -> unit
+  val help_outer_syntax: string list -> unit
   val print_outer_syntax: unit -> unit
   val scan: Position.T -> string -> Token.T list
   val parse: Position.T -> string -> Toplevel.transition list
@@ -62,6 +63,12 @@
   Markup.properties (Position.entity_properties_of def id pos)
     (Markup.entity Markup.commandN name);
 
+fun pretty_command (cmd as (name, Command {comment, ...})) =
+  Pretty.block
+    (Pretty.marks_str
+      ([Sendback.make_markup {implicit = true}, command_markup false cmd], name) ::
+      Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
+
 
 (* parse command *)
 
@@ -114,8 +121,7 @@
   in make_outer_syntax commands' markups' end;
 
 fun dest_commands (Outer_Syntax {commands, ...}) =
-  commands |> Symtab.dest |> sort_wrt #1
-  |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
+  commands |> Symtab.dest |> sort_wrt #1;
 
 fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
 
@@ -196,17 +202,22 @@
 
 (* inspect syntax *)
 
+fun help_outer_syntax pats =
+  dest_commands (#2 (get_syntax ()))
+  |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
+  |> map pretty_command
+  |> Pretty.chunks |> Pretty.writeln;
+
 fun print_outer_syntax () =
   let
     val ((keywords, _), outer_syntax) =
       CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
-    fun pretty_cmd (name, comment, _) =
-      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
-    val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
+    val (int_cmds, cmds) =
+      List.partition (fn (_, Command {int_only, ...}) => int_only) (dest_commands outer_syntax);
   in
     [Pretty.strs ("syntax keywords:" :: map quote keywords),
-      Pretty.big_list "commands:" (map pretty_cmd cmds),
-      Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
+      Pretty.big_list "commands:" (map pretty_command cmds),
+      Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
     |> Pretty.chunks |> Pretty.writeln
   end;