refined outer syntax 'help' command;
authorwenzelm
Mon Nov 26 13:54:43 2012 +0100 (2012-11-26)
changeset 502137b73c0509835
parent 50212 4fb06c22c5ec
child 50214 67fb9a168d10
refined outer syntax 'help' command;
NEWS
src/Doc/IsarRef/Misc.thy
src/Doc/IsarRef/Outer_Syntax.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/NEWS	Mon Nov 26 11:59:56 2012 +0100
     1.2 +++ b/NEWS	Mon Nov 26 13:54:43 2012 +0100
     1.3 @@ -41,6 +41,9 @@
     1.4  * More informative error messages for Isar proof commands involving
     1.5  lazy enumerations (method applications etc.).
     1.6  
     1.7 +* Refined 'help' command to retrieve outer syntax commands according
     1.8 +to name patterns (with clickable results).
     1.9 +
    1.10  
    1.11  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.12  
     2.1 --- a/src/Doc/IsarRef/Misc.thy	Mon Nov 26 11:59:56 2012 +0100
     2.2 +++ b/src/Doc/IsarRef/Misc.thy	Mon Nov 26 13:54:43 2012 +0100
     2.3 @@ -8,7 +8,6 @@
     2.4  
     2.5  text {*
     2.6    \begin{matharray}{rcl}
     2.7 -    @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     2.8      @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     2.9      @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.10      @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.11 @@ -46,9 +45,6 @@
    2.12  
    2.13    \begin{description}
    2.14    
    2.15 -  \item @{command "print_commands"} prints Isabelle's outer theory
    2.16 -  syntax, including keywords and command.
    2.17 -  
    2.18    \item @{command "print_theory"} prints the main logical content of
    2.19    the theory context; the ``@{text "!"}'' option indicates extra
    2.20    verbosity.
     3.1 --- a/src/Doc/IsarRef/Outer_Syntax.thy	Mon Nov 26 11:59:56 2012 +0100
     3.2 +++ b/src/Doc/IsarRef/Outer_Syntax.thy	Mon Nov 26 13:54:43 2012 +0100
     3.3 @@ -64,6 +64,39 @@
     3.4  *}
     3.5  
     3.6  
     3.7 +section {* Commands *}
     3.8 +
     3.9 +text {*
    3.10 +  \begin{matharray}{rcl}
    3.11 +    @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    3.12 +    @{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    3.13 +  \end{matharray}
    3.14 +
    3.15 +  @{rail "
    3.16 +    @@{command help} (@{syntax name} * )
    3.17 +  "}
    3.18 +
    3.19 +  \begin{description}
    3.20 +
    3.21 +  \item @{command "print_commands"} prints all outer syntax keywords
    3.22 +  and commands.
    3.23 +
    3.24 +  \item @{command "help"}~@{text "pats"} retrieves outer syntax
    3.25 +  commands according to the specified name patterns.
    3.26 +
    3.27 +  \end{description}
    3.28 +*}
    3.29 +
    3.30 +
    3.31 +subsubsection {* Examples *}
    3.32 +
    3.33 +text {* Some common diagnostic commands are retrieved like this
    3.34 +  (according to usual naming conventions): *}
    3.35 +
    3.36 +help "print"
    3.37 +help "find"
    3.38 +
    3.39 +
    3.40  section {* Lexical matters \label{sec:outer-lex} *}
    3.41  
    3.42  text {* The outer lexical syntax consists of three main categories of
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Nov 26 11:59:56 2012 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 26 13:54:43 2012 +0100
     4.3 @@ -764,8 +764,10 @@
     4.4        (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
     4.5  
     4.6  val _ =
     4.7 -  Outer_Syntax.improper_command @{command_spec "help"} "print outer syntax commands"
     4.8 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
     4.9 +  Outer_Syntax.improper_command @{command_spec "help"}
    4.10 +    "retrieve outer syntax commands according to name patterns"
    4.11 +    (Scan.repeat Parse.name >> (fn pats =>
    4.12 +      Toplevel.no_timing o Toplevel.imperative (fn () => Outer_Syntax.help_outer_syntax pats)));
    4.13  
    4.14  val _ =
    4.15    Outer_Syntax.improper_command @{command_spec "print_commands"} "print outer syntax commands"
     5.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Nov 26 11:59:56 2012 +0100
     5.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Nov 26 13:54:43 2012 +0100
     5.3 @@ -28,6 +28,7 @@
     5.4      (bool -> local_theory -> Proof.state) parser -> unit
     5.5    val local_theory_to_proof: command_spec -> string ->
     5.6      (local_theory -> Proof.state) parser -> unit
     5.7 +  val help_outer_syntax: string list -> unit
     5.8    val print_outer_syntax: unit -> unit
     5.9    val scan: Position.T -> string -> Token.T list
    5.10    val parse: Position.T -> string -> Toplevel.transition list
    5.11 @@ -62,6 +63,12 @@
    5.12    Markup.properties (Position.entity_properties_of def id pos)
    5.13      (Markup.entity Markup.commandN name);
    5.14  
    5.15 +fun pretty_command (cmd as (name, Command {comment, ...})) =
    5.16 +  Pretty.block
    5.17 +    (Pretty.marks_str
    5.18 +      ([Sendback.make_markup {implicit = true}, command_markup false cmd], name) ::
    5.19 +      Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
    5.20 +
    5.21  
    5.22  (* parse command *)
    5.23  
    5.24 @@ -114,8 +121,7 @@
    5.25    in make_outer_syntax commands' markups' end;
    5.26  
    5.27  fun dest_commands (Outer_Syntax {commands, ...}) =
    5.28 -  commands |> Symtab.dest |> sort_wrt #1
    5.29 -  |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
    5.30 +  commands |> Symtab.dest |> sort_wrt #1;
    5.31  
    5.32  fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
    5.33  
    5.34 @@ -196,17 +202,22 @@
    5.35  
    5.36  (* inspect syntax *)
    5.37  
    5.38 +fun help_outer_syntax pats =
    5.39 +  dest_commands (#2 (get_syntax ()))
    5.40 +  |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
    5.41 +  |> map pretty_command
    5.42 +  |> Pretty.chunks |> Pretty.writeln;
    5.43 +
    5.44  fun print_outer_syntax () =
    5.45    let
    5.46      val ((keywords, _), outer_syntax) =
    5.47        CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
    5.48 -    fun pretty_cmd (name, comment, _) =
    5.49 -      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    5.50 -    val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
    5.51 +    val (int_cmds, cmds) =
    5.52 +      List.partition (fn (_, Command {int_only, ...}) => int_only) (dest_commands outer_syntax);
    5.53    in
    5.54      [Pretty.strs ("syntax keywords:" :: map quote keywords),
    5.55 -      Pretty.big_list "commands:" (map pretty_cmd cmds),
    5.56 -      Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
    5.57 +      Pretty.big_list "commands:" (map pretty_command cmds),
    5.58 +      Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
    5.59      |> Pretty.chunks |> Pretty.writeln
    5.60    end;
    5.61