merged
authorwenzelm
Mon Nov 26 17:13:44 2012 +0100 (2012-11-26)
changeset 5023181a067b188b8
parent 50230 79773c44e57b
parent 50217 ce1f0602f48e
child 50232 289a34f9c383
merged
NEWS
src/HOL/Tools/Lifting/lifting_setup.ML
src/Pure/Tools/xml_syntax.ML
     1.1 --- a/NEWS	Mon Nov 26 16:01:04 2012 +0100
     1.2 +++ b/NEWS	Mon Nov 26 17:13:44 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 16:01:04 2012 +0100
     2.2 +++ b/src/Doc/IsarRef/Misc.thy	Mon Nov 26 17:13:44 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 16:01:04 2012 +0100
     3.2 +++ b/src/Doc/IsarRef/Outer_Syntax.thy	Mon Nov 26 17:13:44 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/HOL/BNF/Tools/bnf_wrap.ML	Mon Nov 26 16:01:04 2012 +0100
     4.2 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Mon Nov 26 17:13:44 2012 +0100
     4.3 @@ -675,7 +675,7 @@
     4.4      >> (pairself (exists I) o split_list)) (false, false);
     4.5  
     4.6  val _ =
     4.7 -  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"
     4.8 +  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wrap an existing datatype"
     4.9      ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
    4.10        Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
    4.11          Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
     5.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Nov 26 16:01:04 2012 +0100
     5.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Nov 26 17:13:44 2012 +0100
     5.3 @@ -302,7 +302,7 @@
     5.4  
     5.5  val _ =
     5.6    Outer_Syntax.command @{command_spec "boogie_vc"}
     5.7 -    "enter into proof mode for a specific verification condition"
     5.8 +    "enter into proof mode for a specific Boogie verification condition"
     5.9      (vc_name -- vc_opts >> (fn args =>
    5.10        (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
    5.11  
    5.12 @@ -334,7 +334,7 @@
    5.13  
    5.14  val _ =
    5.15    Outer_Syntax.improper_command @{command_spec "boogie_status"}
    5.16 -    "show the name and state of all loaded verification conditions"
    5.17 +    "show the name and state of all loaded Boogie verification conditions"
    5.18      (status_test >> status_cmd ||
    5.19       status_vc >> status_cmd ||
    5.20       Scan.succeed (status_cmd boogie_status))
     6.1 --- a/src/HOL/Import/import_data.ML	Mon Nov 26 16:01:04 2012 +0100
     6.2 +++ b/src/HOL/Import/import_data.ML	Mon Nov 26 17:13:44 2012 +0100
     6.3 @@ -104,13 +104,13 @@
     6.4  val type_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
     6.5    (fn (ty_name1, ty_name2) => add_typ_map ty_name1 ty_name2)
     6.6  val _ = Outer_Syntax.command @{command_spec "import_type_map"}
     6.7 -  "Map external type name to existing Isabelle/HOL type name"
     6.8 +  "map external type name to existing Isabelle/HOL type name"
     6.9    (type_map >> Toplevel.theory)
    6.10  
    6.11  val const_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
    6.12    (fn (cname1, cname2) => add_const_map cname1 cname2)
    6.13  val _ = Outer_Syntax.command @{command_spec "import_const_map"}
    6.14 -  "Map external const name to existing Isabelle/HOL const name"
    6.15 +  "map external const name to existing Isabelle/HOL const name"
    6.16    (const_map >> Toplevel.theory)
    6.17  
    6.18  (* Initial type and constant maps, for types and constants that are not
     7.1 --- a/src/HOL/Import/import_rule.ML	Mon Nov 26 16:01:04 2012 +0100
     7.2 +++ b/src/HOL/Import/import_rule.ML	Mon Nov 26 17:13:44 2012 +0100
     7.3 @@ -443,7 +443,7 @@
     7.4    (thy, init_state) |> File.fold_lines process_line path |> fst
     7.5  
     7.6  val _ = Outer_Syntax.command @{command_spec "import_file"}
     7.7 -  "Import a recorded proof file"
     7.8 +  "import a recorded proof file"
     7.9    (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
    7.10  
    7.11  
     8.1 --- a/src/HOL/Statespace/state_space.ML	Mon Nov 26 16:01:04 2012 +0100
     8.2 +++ b/src/HOL/Statespace/state_space.ML	Mon Nov 26 17:13:44 2012 +0100
     8.3 @@ -706,7 +706,7 @@
     8.4          (plus1_unless comp parent --
     8.5            Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
     8.6  val _ =
     8.7 -  Outer_Syntax.command @{command_spec "statespace"} "define state space"
     8.8 +  Outer_Syntax.command @{command_spec "statespace"} "define state-space as locale context"
     8.9      (statespace_decl >> (fn ((args, name), (parents, comps)) =>
    8.10        Toplevel.theory (define_statespace args name parents comps)));
    8.11  
     9.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Nov 26 16:01:04 2012 +0100
     9.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Nov 26 17:13:44 2012 +0100
     9.3 @@ -309,7 +309,7 @@
     9.4  
     9.5  val _ = 
     9.6    Outer_Syntax.local_theory @{command_spec "setup_lifting"}
     9.7 -    "Setup lifting infrastructure" 
     9.8 +    "setup lifting infrastructure" 
     9.9        (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
    9.10          (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm))
    9.11  end;
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 16:01:04 2012 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 17:13:44 2012 +0100
    10.3 @@ -470,7 +470,8 @@
    10.4                pprint_nt (fn () => Pretty.blk (0,
    10.5                    pstrs "Hint: To check that the induction hypothesis is \
    10.6                          \general enough, try this command: " @
    10.7 -                  [Pretty.mark (Sendback.make_markup ()) (Pretty.blk (0,
    10.8 +                  [Pretty.mark (Sendback.make_markup {implicit = false, properties = []})
    10.9 +                    (Pretty.blk (0,
   10.10                         pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
   10.11              else
   10.12                ()
    11.1 --- a/src/HOL/Tools/inductive.ML	Mon Nov 26 16:01:04 2012 +0100
    11.2 +++ b/src/HOL/Tools/inductive.ML	Mon Nov 26 17:13:44 2012 +0100
    11.3 @@ -1157,7 +1157,7 @@
    11.4  
    11.5  val _ =
    11.6    Outer_Syntax.local_theory @{command_spec "inductive_cases"}
    11.7 -    "create simplified instances of elimination rules (improper)"
    11.8 +    "create simplified instances of elimination rules"
    11.9      (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
   11.10  
   11.11  val _ =
    12.1 --- a/src/HOL/Tools/recdef.ML	Mon Nov 26 16:01:04 2012 +0100
    12.2 +++ b/src/HOL/Tools/recdef.ML	Mon Nov 26 17:13:44 2012 +0100
    12.3 @@ -302,7 +302,7 @@
    12.4    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
    12.5  
    12.6  val _ =
    12.7 -  Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (TFL)"
    12.8 +  Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)"
    12.9      (recdef_decl >> Toplevel.theory);
   12.10  
   12.11  
   12.12 @@ -314,12 +314,12 @@
   12.13  
   12.14  val _ =
   12.15    Outer_Syntax.command @{command_spec "defer_recdef"}
   12.16 -    "defer general recursive functions (TFL)"
   12.17 +    "defer general recursive functions (obsolete TFL)"
   12.18      (defer_recdef_decl >> Toplevel.theory);
   12.19  
   12.20  val _ =
   12.21    Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
   12.22 -    "recommence proof of termination condition (TFL)"
   12.23 +    "recommence proof of termination condition (obsolete TFL)"
   12.24      ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
   12.25          Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
   12.26        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
    13.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Nov 26 16:01:04 2012 +0100
    13.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 26 17:13:44 2012 +0100
    13.3 @@ -134,11 +134,11 @@
    13.4    Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
    13.5  
    13.6  val _ =
    13.7 -  Outer_Syntax.command @{command_spec "syntax"} "declare syntactic constants"
    13.8 +  Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
    13.9      (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
   13.10  
   13.11  val _ =
   13.12 -  Outer_Syntax.command @{command_spec "no_syntax"} "delete syntax declarations"
   13.13 +  Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
   13.14      (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
   13.15  
   13.16  
   13.17 @@ -159,11 +159,11 @@
   13.18      >> (fn (left, (arr, right)) => arr (left, right));
   13.19  
   13.20  val _ =
   13.21 -  Outer_Syntax.command @{command_spec "translations"} "declare syntax translation rules"
   13.22 +  Outer_Syntax.command @{command_spec "translations"} "add syntax translation rules"
   13.23      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
   13.24  
   13.25  val _ =
   13.26 -  Outer_Syntax.command @{command_spec "no_translations"} "remove syntax translation rules"
   13.27 +  Outer_Syntax.command @{command_spec "no_translations"} "delete syntax translation rules"
   13.28      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
   13.29  
   13.30  
   13.31 @@ -538,7 +538,7 @@
   13.32      (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
   13.33  
   13.34  val _ =
   13.35 -  Outer_Syntax.command @{command_spec "hence"} "abbreviates \"then have\""
   13.36 +  Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
   13.37      (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
   13.38  
   13.39  val _ =
   13.40 @@ -547,7 +547,7 @@
   13.41      (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
   13.42  
   13.43  val _ =
   13.44 -  Outer_Syntax.command @{command_spec "thus"} "abbreviates \"then show\""
   13.45 +  Outer_Syntax.command @{command_spec "thus"} "old-style alias of  \"then show\""
   13.46      (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
   13.47  
   13.48  
   13.49 @@ -595,7 +595,7 @@
   13.50      (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
   13.51  
   13.52  val _ =
   13.53 -  Outer_Syntax.command @{command_spec "def"} "local definition"
   13.54 +  Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
   13.55      (Parse.and_list1
   13.56        (Parse_Spec.opt_thm_name ":" --
   13.57          ((Parse.binding -- Parse.opt_mixfix) --
   13.58 @@ -649,7 +649,7 @@
   13.59  (* end proof *)
   13.60  
   13.61  val _ =
   13.62 -  Outer_Syntax.command @{command_spec "qed"} "conclude (sub-)proof"
   13.63 +  Outer_Syntax.command @{command_spec "qed"} "conclude proof"
   13.64      (Scan.option Method.parse >> Isar_Cmd.qed);
   13.65  
   13.66  val _ =
   13.67 @@ -692,11 +692,11 @@
   13.68      (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
   13.69  
   13.70  val _ =
   13.71 -  Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement (unstructured)"
   13.72 +  Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
   13.73      (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
   13.74  
   13.75  val _ =
   13.76 -  Outer_Syntax.command @{command_spec "proof"} "backward proof"
   13.77 +  Outer_Syntax.command @{command_spec "proof"} "backward proof step"
   13.78      (Scan.option Method.parse >> (fn m => Toplevel.print o
   13.79        Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
   13.80        Toplevel.skip_proof (fn i => i + 1)));
   13.81 @@ -741,7 +741,7 @@
   13.82        (Position.of_properties (Position.default_properties pos props), str));
   13.83  
   13.84  val _ =
   13.85 -  Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "nested Isabelle command"
   13.86 +  Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command"
   13.87      (props_text :|-- (fn (pos, str) =>
   13.88        (case Outer_Syntax.parse pos str of
   13.89          [tr] => Scan.succeed (K tr)
   13.90 @@ -764,8 +764,10 @@
   13.91        (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
   13.92  
   13.93  val _ =
   13.94 -  Outer_Syntax.improper_command @{command_spec "help"} "print outer syntax commands"
   13.95 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
   13.96 +  Outer_Syntax.improper_command @{command_spec "help"}
   13.97 +    "retrieve outer syntax commands according to name patterns"
   13.98 +    (Scan.repeat Parse.name >> (fn pats =>
   13.99 +      Toplevel.no_timing o Toplevel.imperative (fn () => Outer_Syntax.help_outer_syntax pats)));
  13.100  
  13.101  val _ =
  13.102    Outer_Syntax.improper_command @{command_spec "print_commands"} "print outer syntax commands"
  13.103 @@ -849,8 +851,7 @@
  13.104      (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
  13.105  
  13.106  val _ =
  13.107 -  Outer_Syntax.improper_command @{command_spec "print_antiquotations"}
  13.108 -    "print antiquotations (global)"
  13.109 +  Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
  13.110      (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
  13.111  
  13.112  val _ =
  13.113 @@ -984,7 +985,7 @@
  13.114  
  13.115  val _ =
  13.116    Outer_Syntax.improper_command @{command_spec "commit"}
  13.117 -    "commit current session to ML database"
  13.118 +    "commit current session to ML session image"
  13.119      (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
  13.120  
  13.121  val _ =
    14.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Nov 26 16:01:04 2012 +0100
    14.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Nov 26 17:13:44 2012 +0100
    14.3 @@ -28,6 +28,7 @@
    14.4      (bool -> local_theory -> Proof.state) parser -> unit
    14.5    val local_theory_to_proof: command_spec -> string ->
    14.6      (local_theory -> Proof.state) parser -> unit
    14.7 +  val help_outer_syntax: string list -> unit
    14.8    val print_outer_syntax: unit -> unit
    14.9    val scan: Position.T -> string -> Token.T list
   14.10    val parse: Position.T -> string -> Toplevel.transition list
   14.11 @@ -62,6 +63,12 @@
   14.12    Markup.properties (Position.entity_properties_of def id pos)
   14.13      (Markup.entity Markup.commandN name);
   14.14  
   14.15 +fun pretty_command (cmd as (name, Command {comment, ...})) =
   14.16 +  Pretty.block
   14.17 +    (Pretty.marks_str
   14.18 +      ([Sendback.make_markup {implicit = true, properties = [Markup.padding_line]},
   14.19 +        command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   14.20 +
   14.21  
   14.22  (* parse command *)
   14.23  
   14.24 @@ -114,8 +121,7 @@
   14.25    in make_outer_syntax commands' markups' end;
   14.26  
   14.27  fun dest_commands (Outer_Syntax {commands, ...}) =
   14.28 -  commands |> Symtab.dest |> sort_wrt #1
   14.29 -  |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
   14.30 +  commands |> Symtab.dest |> sort_wrt #1;
   14.31  
   14.32  fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
   14.33  
   14.34 @@ -196,17 +202,22 @@
   14.35  
   14.36  (* inspect syntax *)
   14.37  
   14.38 +fun help_outer_syntax pats =
   14.39 +  dest_commands (#2 (get_syntax ()))
   14.40 +  |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
   14.41 +  |> map pretty_command
   14.42 +  |> Pretty.chunks |> Pretty.writeln;
   14.43 +
   14.44  fun print_outer_syntax () =
   14.45    let
   14.46      val ((keywords, _), outer_syntax) =
   14.47        CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
   14.48 -    fun pretty_cmd (name, comment, _) =
   14.49 -      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   14.50 -    val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
   14.51 +    val (int_cmds, cmds) =
   14.52 +      List.partition (fn (_, Command {int_only, ...}) => int_only) (dest_commands outer_syntax);
   14.53    in
   14.54      [Pretty.strs ("syntax keywords:" :: map quote keywords),
   14.55 -      Pretty.big_list "commands:" (map pretty_cmd cmds),
   14.56 -      Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
   14.57 +      Pretty.big_list "commands:" (map pretty_command cmds),
   14.58 +      Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
   14.59      |> Pretty.chunks |> Pretty.writeln
   14.60    end;
   14.61  
    15.1 --- a/src/Pure/PIDE/markup.ML	Mon Nov 26 16:01:04 2012 +0100
    15.2 +++ b/src/Pure/PIDE/markup.ML	Mon Nov 26 17:13:44 2012 +0100
    15.3 @@ -96,6 +96,8 @@
    15.4    val proof_stateN: string val proof_state: int -> T
    15.5    val stateN: string val state: T
    15.6    val subgoalN: string val subgoal: T
    15.7 +  val paddingN: string
    15.8 +  val padding_line: string * string
    15.9    val sendbackN: string val sendback: T
   15.10    val intensifyN: string val intensify: T
   15.11    val taskN: string
   15.12 @@ -333,7 +335,11 @@
   15.13  
   15.14  val (stateN, state) = markup_elem "state";
   15.15  val (subgoalN, subgoal) = markup_elem "subgoal";
   15.16 +
   15.17 +val paddingN = "padding";
   15.18 +val padding_line = (paddingN, lineN);
   15.19  val (sendbackN, sendback) = markup_elem "sendback";
   15.20 +
   15.21  val (intensifyN, intensify) = markup_elem "intensify";
   15.22  
   15.23  
    16.1 --- a/src/Pure/PIDE/markup.scala	Mon Nov 26 16:01:04 2012 +0100
    16.2 +++ b/src/Pure/PIDE/markup.scala	Mon Nov 26 17:13:44 2012 +0100
    16.3 @@ -211,7 +211,11 @@
    16.4  
    16.5    val STATE = "state"
    16.6    val SUBGOAL = "subgoal"
    16.7 +
    16.8 +  val PADDING = "padding"
    16.9 +  val PADDING_LINE = (PADDING, LINE)
   16.10    val SENDBACK = "sendback"
   16.11 +
   16.12    val INTENSIFY = "intensify"
   16.13  
   16.14  
    17.1 --- a/src/Pure/PIDE/sendback.ML	Mon Nov 26 16:01:04 2012 +0100
    17.2 +++ b/src/Pure/PIDE/sendback.ML	Mon Nov 26 17:13:44 2012 +0100
    17.3 @@ -7,25 +7,27 @@
    17.4  
    17.5  signature SENDBACK =
    17.6  sig
    17.7 -  val make_markup: unit -> Markup.T
    17.8 +  val make_markup: {implicit: bool, properties: Properties.T} -> Markup.T
    17.9 +  val markup_implicit: string -> string
   17.10    val markup: string -> string
   17.11 -  val markup_implicit: string -> string
   17.12  end;
   17.13  
   17.14  structure Sendback: SENDBACK =
   17.15  struct
   17.16  
   17.17 -fun make_markup () =
   17.18 -  let
   17.19 -    val props =
   17.20 -      (case Position.get_id (Position.thread_data ()) of
   17.21 -        SOME id => [(Markup.idN, id)]
   17.22 -      | NONE => []);
   17.23 -  in Markup.properties props Markup.sendback end;
   17.24 +fun make_markup {implicit, properties} =
   17.25 +  Markup.sendback
   17.26 +  |> not implicit ? (fn markup =>
   17.27 +      let
   17.28 +        val props =
   17.29 +          (case Position.get_id (Position.thread_data ()) of
   17.30 +            SOME id => [(Markup.idN, id)]
   17.31 +          | NONE => []);
   17.32 +      in Markup.properties props markup end)
   17.33 +  |> Markup.properties properties;
   17.34  
   17.35 -fun markup s = Markup.markup (make_markup ()) s;
   17.36 -
   17.37 -fun markup_implicit s = Markup.markup Markup.sendback s;
   17.38 +fun markup_implicit s = Markup.markup (make_markup {implicit = true, properties = []}) s;
   17.39 +fun markup s = Markup.markup (make_markup {implicit = false, properties = []}) s;
   17.40  
   17.41  end;
   17.42  
    18.1 --- a/src/Pure/ROOT	Mon Nov 26 16:01:04 2012 +0100
    18.2 +++ b/src/Pure/ROOT	Mon Nov 26 17:13:44 2012 +0100
    18.3 @@ -200,7 +200,7 @@
    18.4      "Thy/thy_output.ML"
    18.5      "Thy/thy_syntax.ML"
    18.6      "Tools/named_thms.ML"
    18.7 -    "Tools/xml_syntax.ML"
    18.8 +    "Tools/legacy_xml_syntax.ML"
    18.9      "assumption.ML"
   18.10      "axclass.ML"
   18.11      "config.ML"
    19.1 --- a/src/Pure/ROOT.ML	Mon Nov 26 16:01:04 2012 +0100
    19.2 +++ b/src/Pure/ROOT.ML	Mon Nov 26 17:13:44 2012 +0100
    19.3 @@ -283,7 +283,7 @@
    19.4  
    19.5  use "Tools/named_thms.ML";
    19.6  
    19.7 -use "Tools/xml_syntax.ML";
    19.8 +use "Tools/legacy_xml_syntax.ML";
    19.9  
   19.10  
   19.11  (* configuration for Proof General *)
    20.1 --- a/src/Pure/Tools/find_consts.ML	Mon Nov 26 16:01:04 2012 +0100
    20.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Nov 26 17:13:44 2012 +0100
    20.3 @@ -136,7 +136,8 @@
    20.4  in
    20.5  
    20.6  val _ =
    20.7 -  Outer_Syntax.improper_command @{command_spec "find_consts"} "search constants by type pattern"
    20.8 +  Outer_Syntax.improper_command @{command_spec "find_consts"}
    20.9 +    "find constants by name/type patterns"
   20.10      (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
   20.11        >> (fn spec => Toplevel.no_timing o
   20.12          Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
    21.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Nov 26 16:01:04 2012 +0100
    21.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Nov 26 17:13:44 2012 +0100
    21.3 @@ -116,17 +116,17 @@
    21.4    | xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
    21.5    | xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
    21.6    | xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
    21.7 -  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []) , [XML_Syntax.xml_of_term pat])
    21.8 -  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []) , [XML_Syntax.xml_of_term pat]);
    21.9 +  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []), [Legacy_XML_Syntax.xml_of_term pat])
   21.10 +  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []), [Legacy_XML_Syntax.xml_of_term pat]);
   21.11  
   21.12  fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
   21.13    | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
   21.14    | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
   21.15    | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
   21.16    | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
   21.17 -  | criterion_of_xml (XML.Elem (("Simp", []) , [tree])) = Simp (XML_Syntax.term_of_xml tree)
   21.18 -  | criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
   21.19 -  | criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
   21.20 +  | criterion_of_xml (XML.Elem (("Simp", []), [tree])) = Simp (Legacy_XML_Syntax.term_of_xml tree)
   21.21 +  | criterion_of_xml (XML.Elem (("Pattern", []), [tree])) = Pattern (Legacy_XML_Syntax.term_of_xml tree)
   21.22 +  | criterion_of_xml tree = raise Legacy_XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
   21.23  
   21.24  fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
   21.25        let
   21.26 @@ -149,7 +149,7 @@
   21.27        in
   21.28          {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
   21.29        end
   21.30 -  | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
   21.31 +  | query_of_xml tree = raise Legacy_XML_Syntax.XML ("query_of_xml: bad tree", tree);
   21.32  
   21.33  
   21.34  
   21.35 @@ -167,7 +167,7 @@
   21.36  
   21.37  fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
   21.38    | xml_of_theorem (External (fact_ref, prop)) =
   21.39 -      XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop]);
   21.40 +      XML.Elem (fact_ref_markup fact_ref ("External", []), [Legacy_XML_Syntax.xml_of_term prop]);
   21.41  
   21.42  fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
   21.43        let
   21.44 @@ -177,9 +177,9 @@
   21.45            Option.map (single o Facts.Single o Markup.parse_int)
   21.46              (Properties.get properties "index");
   21.47        in
   21.48 -        External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
   21.49 +        External (Facts.Named ((name, pos), intvs_opt), Legacy_XML_Syntax.term_of_xml tree)
   21.50        end
   21.51 -  | theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
   21.52 +  | theorem_of_xml tree = raise Legacy_XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
   21.53  
   21.54  fun xml_of_result (opt_found, theorems) =
   21.55    let
   21.56 @@ -192,7 +192,7 @@
   21.57  fun result_of_xml (XML.Elem (("Result", properties), body)) =
   21.58        (Properties.get properties "found" |> Option.map Markup.parse_int,
   21.59         XML.Decode.list (theorem_of_xml o the_single) body)
   21.60 -  | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
   21.61 +  | result_of_xml tree = raise Legacy_XML_Syntax.XML ("result_of_xml: bad tree", tree);
   21.62  
   21.63  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
   21.64    | prop_of (External (_, prop)) = prop;
   21.65 @@ -625,7 +625,7 @@
   21.66  
   21.67  val _ =
   21.68    Outer_Syntax.improper_command @{command_spec "find_theorems"}
   21.69 -    "print theorems meeting specified criteria"
   21.70 +    "find theorems meeting specified criteria"
   21.71      (options -- query_parser
   21.72        >> (fn ((opt_lim, rem_dups), spec) =>
   21.73          Toplevel.no_timing o
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/Pure/Tools/legacy_xml_syntax.ML	Mon Nov 26 17:13:44 2012 +0100
    22.3 @@ -0,0 +1,173 @@
    22.4 +(*  Title:      Pure/Tools/legacy_xml_syntax.ML
    22.5 +    Author:     Stefan Berghofer, TU Muenchen
    22.6 +
    22.7 +Input and output of types, terms, and proofs in XML format.
    22.8 +See isabelle.xsd for a description of the syntax.
    22.9 +
   22.10 +Legacy module, see Pure/term_xml.ML etc.
   22.11 +*)
   22.12 +
   22.13 +signature LEGACY_XML_SYNTAX =
   22.14 +sig
   22.15 +  val xml_of_type: typ -> XML.tree
   22.16 +  val xml_of_term: term -> XML.tree
   22.17 +  val xml_of_proof: Proofterm.proof -> XML.tree
   22.18 +  val write_to_file: Path.T -> string -> XML.tree -> unit
   22.19 +  exception XML of string * XML.tree
   22.20 +  val type_of_xml: XML.tree -> typ
   22.21 +  val term_of_xml: XML.tree -> term
   22.22 +  val proof_of_xml: XML.tree -> Proofterm.proof
   22.23 +end;
   22.24 +
   22.25 +structure Legacy_XML_Syntax : LEGACY_XML_SYNTAX =
   22.26 +struct
   22.27 +
   22.28 +(**** XML output ****)
   22.29 +
   22.30 +fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
   22.31 +
   22.32 +fun xml_of_type (TVar ((s, i), S)) =
   22.33 +      XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
   22.34 +        map xml_of_class S)
   22.35 +  | xml_of_type (TFree (s, S)) =
   22.36 +      XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
   22.37 +  | xml_of_type (Type (s, Ts)) =
   22.38 +      XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
   22.39 +
   22.40 +fun xml_of_term (Bound i) =
   22.41 +      XML.Elem (("Bound", [("index", string_of_int i)]), [])
   22.42 +  | xml_of_term (Free (s, T)) =
   22.43 +      XML.Elem (("Free", [("name", s)]), [xml_of_type T])
   22.44 +  | xml_of_term (Var ((s, i), T)) =
   22.45 +      XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
   22.46 +        [xml_of_type T])
   22.47 +  | xml_of_term (Const (s, T)) =
   22.48 +      XML.Elem (("Const", [("name", s)]), [xml_of_type T])
   22.49 +  | xml_of_term (t $ u) =
   22.50 +      XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
   22.51 +  | xml_of_term (Abs (s, T, t)) =
   22.52 +      XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
   22.53 +
   22.54 +fun xml_of_opttypes NONE = []
   22.55 +  | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
   22.56 +
   22.57 +(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
   22.58 +(* it can be looked up in the theorem database. Thus, it could be      *)
   22.59 +(* omitted from the xml representation.                                *)
   22.60 +
   22.61 +(* FIXME not exhaustive *)
   22.62 +fun xml_of_proof (PBound i) =
   22.63 +      XML.Elem (("PBound", [("index", string_of_int i)]), [])
   22.64 +  | xml_of_proof (Abst (s, optT, prf)) =
   22.65 +      XML.Elem (("Abst", [("vname", s)]),
   22.66 +        (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
   22.67 +  | xml_of_proof (AbsP (s, optt, prf)) =
   22.68 +      XML.Elem (("AbsP", [("vname", s)]),
   22.69 +        (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
   22.70 +  | xml_of_proof (prf % optt) =
   22.71 +      XML.Elem (("Appt", []),
   22.72 +        xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
   22.73 +  | xml_of_proof (prf %% prf') =
   22.74 +      XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
   22.75 +  | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
   22.76 +  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
   22.77 +      XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   22.78 +  | xml_of_proof (PAxm (s, t, optTs)) =
   22.79 +      XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   22.80 +  | xml_of_proof (Oracle (s, t, optTs)) =
   22.81 +      XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   22.82 +  | xml_of_proof MinProof =
   22.83 +      XML.Elem (("MinProof", []), []);
   22.84 +
   22.85 +
   22.86 +(* useful for checking the output against a schema file *)
   22.87 +
   22.88 +fun write_to_file path elname x =
   22.89 +  File.write path
   22.90 +    ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
   22.91 +     XML.string_of (XML.Elem ((elname,
   22.92 +         [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
   22.93 +          ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
   22.94 +       [x])));
   22.95 +
   22.96 +
   22.97 +
   22.98 +(**** XML input ****)
   22.99 +
  22.100 +exception XML of string * XML.tree;
  22.101 +
  22.102 +fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
  22.103 +  | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
  22.104 +
  22.105 +fun index_of_string s tree idx =
  22.106 +  (case Int.fromString idx of
  22.107 +    NONE => raise XML (s ^ ": bad index", tree)
  22.108 +  | SOME i => i);
  22.109 +
  22.110 +fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
  22.111 +      ((case Properties.get atts "name" of
  22.112 +          NONE => raise XML ("type_of_xml: name of TVar missing", tree)
  22.113 +        | SOME name => name,
  22.114 +        the_default 0 (Option.map (index_of_string "type_of_xml" tree)
  22.115 +          (Properties.get atts "index"))),
  22.116 +       map class_of_xml classes)
  22.117 +  | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
  22.118 +      TFree (s, map class_of_xml classes)
  22.119 +  | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
  22.120 +      Type (s, map type_of_xml types)
  22.121 +  | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
  22.122 +
  22.123 +fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
  22.124 +      Bound (index_of_string "bad variable index" tree idx)
  22.125 +  | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
  22.126 +      Free (s, type_of_xml typ)
  22.127 +  | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
  22.128 +      ((case Properties.get atts "name" of
  22.129 +          NONE => raise XML ("type_of_xml: name of Var missing", tree)
  22.130 +        | SOME name => name,
  22.131 +        the_default 0 (Option.map (index_of_string "term_of_xml" tree)
  22.132 +          (Properties.get atts "index"))),
  22.133 +       type_of_xml typ)
  22.134 +  | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
  22.135 +      Const (s, type_of_xml typ)
  22.136 +  | term_of_xml (XML.Elem (("App", []), [term, term'])) =
  22.137 +      term_of_xml term $ term_of_xml term'
  22.138 +  | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
  22.139 +      Abs (s, type_of_xml typ, term_of_xml term)
  22.140 +  | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
  22.141 +
  22.142 +fun opttypes_of_xml [] = NONE
  22.143 +  | opttypes_of_xml [XML.Elem (("types", []), types)] =
  22.144 +      SOME (map type_of_xml types)
  22.145 +  | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
  22.146 +
  22.147 +fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
  22.148 +      PBound (index_of_string "proof_of_xml" tree idx)
  22.149 +  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
  22.150 +      Abst (s, NONE, proof_of_xml proof)
  22.151 +  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
  22.152 +      Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
  22.153 +  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
  22.154 +      AbsP (s, NONE, proof_of_xml proof)
  22.155 +  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
  22.156 +      AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
  22.157 +  | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
  22.158 +      proof_of_xml proof % NONE
  22.159 +  | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
  22.160 +      proof_of_xml proof % SOME (term_of_xml term)
  22.161 +  | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
  22.162 +      proof_of_xml proof %% proof_of_xml proof'
  22.163 +  | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
  22.164 +      Hyp (term_of_xml term)
  22.165 +  | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
  22.166 +      (* FIXME? *)
  22.167 +      PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
  22.168 +        Future.value (Proofterm.approximate_proof_body MinProof)))
  22.169 +  | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
  22.170 +      PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
  22.171 +  | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
  22.172 +      Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
  22.173 +  | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
  22.174 +  | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
  22.175 +
  22.176 +end;
    23.1 --- a/src/Pure/Tools/xml_syntax.ML	Mon Nov 26 16:01:04 2012 +0100
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,171 +0,0 @@
    23.4 -(*  Title:      Pure/Tools/xml_syntax.ML
    23.5 -    Author:     Stefan Berghofer, TU Muenchen
    23.6 -
    23.7 -Input and output of types, terms, and proofs in XML format.
    23.8 -See isabelle.xsd for a description of the syntax.
    23.9 -*)
   23.10 -
   23.11 -signature XML_SYNTAX =
   23.12 -sig
   23.13 -  val xml_of_type: typ -> XML.tree
   23.14 -  val xml_of_term: term -> XML.tree
   23.15 -  val xml_of_proof: Proofterm.proof -> XML.tree
   23.16 -  val write_to_file: Path.T -> string -> XML.tree -> unit
   23.17 -  exception XML of string * XML.tree
   23.18 -  val type_of_xml: XML.tree -> typ
   23.19 -  val term_of_xml: XML.tree -> term
   23.20 -  val proof_of_xml: XML.tree -> Proofterm.proof
   23.21 -end;
   23.22 -
   23.23 -structure XML_Syntax : XML_SYNTAX =
   23.24 -struct
   23.25 -
   23.26 -(**** XML output ****)
   23.27 -
   23.28 -fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
   23.29 -
   23.30 -fun xml_of_type (TVar ((s, i), S)) =
   23.31 -      XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
   23.32 -        map xml_of_class S)
   23.33 -  | xml_of_type (TFree (s, S)) =
   23.34 -      XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
   23.35 -  | xml_of_type (Type (s, Ts)) =
   23.36 -      XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
   23.37 -
   23.38 -fun xml_of_term (Bound i) =
   23.39 -      XML.Elem (("Bound", [("index", string_of_int i)]), [])
   23.40 -  | xml_of_term (Free (s, T)) =
   23.41 -      XML.Elem (("Free", [("name", s)]), [xml_of_type T])
   23.42 -  | xml_of_term (Var ((s, i), T)) =
   23.43 -      XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
   23.44 -        [xml_of_type T])
   23.45 -  | xml_of_term (Const (s, T)) =
   23.46 -      XML.Elem (("Const", [("name", s)]), [xml_of_type T])
   23.47 -  | xml_of_term (t $ u) =
   23.48 -      XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
   23.49 -  | xml_of_term (Abs (s, T, t)) =
   23.50 -      XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
   23.51 -
   23.52 -fun xml_of_opttypes NONE = []
   23.53 -  | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
   23.54 -
   23.55 -(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
   23.56 -(* it can be looked up in the theorem database. Thus, it could be      *)
   23.57 -(* omitted from the xml representation.                                *)
   23.58 -
   23.59 -(* FIXME not exhaustive *)
   23.60 -fun xml_of_proof (PBound i) =
   23.61 -      XML.Elem (("PBound", [("index", string_of_int i)]), [])
   23.62 -  | xml_of_proof (Abst (s, optT, prf)) =
   23.63 -      XML.Elem (("Abst", [("vname", s)]),
   23.64 -        (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
   23.65 -  | xml_of_proof (AbsP (s, optt, prf)) =
   23.66 -      XML.Elem (("AbsP", [("vname", s)]),
   23.67 -        (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
   23.68 -  | xml_of_proof (prf % optt) =
   23.69 -      XML.Elem (("Appt", []),
   23.70 -        xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
   23.71 -  | xml_of_proof (prf %% prf') =
   23.72 -      XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
   23.73 -  | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
   23.74 -  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
   23.75 -      XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   23.76 -  | xml_of_proof (PAxm (s, t, optTs)) =
   23.77 -      XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   23.78 -  | xml_of_proof (Oracle (s, t, optTs)) =
   23.79 -      XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
   23.80 -  | xml_of_proof MinProof =
   23.81 -      XML.Elem (("MinProof", []), []);
   23.82 -
   23.83 -
   23.84 -(* useful for checking the output against a schema file *)
   23.85 -
   23.86 -fun write_to_file path elname x =
   23.87 -  File.write path
   23.88 -    ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
   23.89 -     XML.string_of (XML.Elem ((elname,
   23.90 -         [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
   23.91 -          ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
   23.92 -       [x])));
   23.93 -
   23.94 -
   23.95 -
   23.96 -(**** XML input ****)
   23.97 -
   23.98 -exception XML of string * XML.tree;
   23.99 -
  23.100 -fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
  23.101 -  | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
  23.102 -
  23.103 -fun index_of_string s tree idx =
  23.104 -  (case Int.fromString idx of
  23.105 -    NONE => raise XML (s ^ ": bad index", tree)
  23.106 -  | SOME i => i);
  23.107 -
  23.108 -fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
  23.109 -      ((case Properties.get atts "name" of
  23.110 -          NONE => raise XML ("type_of_xml: name of TVar missing", tree)
  23.111 -        | SOME name => name,
  23.112 -        the_default 0 (Option.map (index_of_string "type_of_xml" tree)
  23.113 -          (Properties.get atts "index"))),
  23.114 -       map class_of_xml classes)
  23.115 -  | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
  23.116 -      TFree (s, map class_of_xml classes)
  23.117 -  | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
  23.118 -      Type (s, map type_of_xml types)
  23.119 -  | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
  23.120 -
  23.121 -fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
  23.122 -      Bound (index_of_string "bad variable index" tree idx)
  23.123 -  | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
  23.124 -      Free (s, type_of_xml typ)
  23.125 -  | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
  23.126 -      ((case Properties.get atts "name" of
  23.127 -          NONE => raise XML ("type_of_xml: name of Var missing", tree)
  23.128 -        | SOME name => name,
  23.129 -        the_default 0 (Option.map (index_of_string "term_of_xml" tree)
  23.130 -          (Properties.get atts "index"))),
  23.131 -       type_of_xml typ)
  23.132 -  | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
  23.133 -      Const (s, type_of_xml typ)
  23.134 -  | term_of_xml (XML.Elem (("App", []), [term, term'])) =
  23.135 -      term_of_xml term $ term_of_xml term'
  23.136 -  | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
  23.137 -      Abs (s, type_of_xml typ, term_of_xml term)
  23.138 -  | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
  23.139 -
  23.140 -fun opttypes_of_xml [] = NONE
  23.141 -  | opttypes_of_xml [XML.Elem (("types", []), types)] =
  23.142 -      SOME (map type_of_xml types)
  23.143 -  | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
  23.144 -
  23.145 -fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
  23.146 -      PBound (index_of_string "proof_of_xml" tree idx)
  23.147 -  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
  23.148 -      Abst (s, NONE, proof_of_xml proof)
  23.149 -  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
  23.150 -      Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
  23.151 -  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
  23.152 -      AbsP (s, NONE, proof_of_xml proof)
  23.153 -  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
  23.154 -      AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
  23.155 -  | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
  23.156 -      proof_of_xml proof % NONE
  23.157 -  | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
  23.158 -      proof_of_xml proof % SOME (term_of_xml term)
  23.159 -  | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
  23.160 -      proof_of_xml proof %% proof_of_xml proof'
  23.161 -  | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
  23.162 -      Hyp (term_of_xml term)
  23.163 -  | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
  23.164 -      (* FIXME? *)
  23.165 -      PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
  23.166 -        Future.value (Proofterm.approximate_proof_body MinProof)))
  23.167 -  | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
  23.168 -      PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
  23.169 -  | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
  23.170 -      Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
  23.171 -  | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
  23.172 -  | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
  23.173 -
  23.174 -end;
    24.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 26 16:01:04 2012 +0100
    24.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 26 17:13:44 2012 +0100
    24.3 @@ -105,6 +105,13 @@
    24.4    }
    24.5  
    24.6  
    24.7 +  /* get text */
    24.8 +
    24.9 +  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
   24.10 +    try { Some(buffer.getText(range.start, range.length)) }
   24.11 +    catch { case _: ArrayIndexOutOfBoundsException => None }
   24.12 +
   24.13 +
   24.14    /* point range */
   24.15  
   24.16    def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
    25.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 26 16:01:04 2012 +0100
    25.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 26 17:13:44 2012 +0100
    25.3 @@ -93,6 +93,7 @@
    25.4            Swing_Thread.later {
    25.5              current_rendering = rendering
    25.6              JEdit_Lib.buffer_edit(getBuffer) {
    25.7 +              rich_text_area.active_reset()
    25.8                getBuffer.setReadOnly(false)
    25.9                setText(text)
   25.10                setCaretPosition(0)
    26.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Nov 26 16:01:04 2012 +0100
    26.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Nov 26 17:13:44 2012 +0100
    26.3 @@ -249,11 +249,11 @@
    26.4    }
    26.5  
    26.6  
    26.7 -  def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
    26.8 +  def sendback(range: Text.Range): Option[Text.Info[Properties.T]] =
    26.9      snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
   26.10          {
   26.11            case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
   26.12 -            Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
   26.13 +            Text.Info(snapshot.convert(info_range), props)
   26.14          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   26.15  
   26.16  
    27.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 16:01:04 2012 +0100
    27.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 17:13:44 2012 +0100
    27.3 @@ -134,11 +134,11 @@
    27.4  
    27.5    private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
    27.6    private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
    27.7 -  private val sendback_area = new Active_Area[Option[Document.Exec_ID]]((r: Rendering) => r.sendback _)
    27.8 +  private val sendback_area = new Active_Area[Properties.T]((r: Rendering) => r.sendback _)
    27.9  
   27.10    private val active_areas =
   27.11      List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
   27.12 -  private def active_reset(): Unit = active_areas.foreach(_._1.reset)
   27.13 +  def active_reset(): Unit = active_areas.foreach(_._1.reset)
   27.14  
   27.15    private val focus_listener = new FocusAdapter {
   27.16      override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
   27.17 @@ -157,7 +157,7 @@
   27.18            case None =>
   27.19          }
   27.20          sendback_area.text_info match {
   27.21 -          case Some((text, Text.Info(_, id))) => Sendback.activate(view, text, id)
   27.22 +          case Some((text, Text.Info(_, props))) => Sendback.activate(view, text, props)
   27.23            case None =>
   27.24          }
   27.25        }
   27.26 @@ -172,7 +172,7 @@
   27.27          if ((control || hovering) && !buffer.isLoading) {
   27.28            JEdit_Lib.buffer_lock(buffer) {
   27.29              JEdit_Lib.pixel_range(text_area, e.getX(), e.getY()) match {
   27.30 -              case None =>
   27.31 +              case None => active_reset()
   27.32                case Some(range) =>
   27.33                  val rendering = get_rendering()
   27.34                  for ((area, require_control) <- active_areas)
    28.1 --- a/src/Tools/jEdit/src/sendback.scala	Mon Nov 26 16:01:04 2012 +0100
    28.2 +++ b/src/Tools/jEdit/src/sendback.scala	Mon Nov 26 17:13:44 2012 +0100
    28.3 @@ -14,22 +14,21 @@
    28.4  
    28.5  object Sendback
    28.6  {
    28.7 -  def activate(view: View, text: String, id: Option[Document.Exec_ID])
    28.8 +  def activate(view: View, text: String, props: Properties.T)
    28.9    {
   28.10      Swing_Thread.require()
   28.11  
   28.12      Document_View(view.getTextArea) match {
   28.13        case Some(doc_view) =>
   28.14          doc_view.rich_text_area.robust_body() {
   28.15 +          val text_area = doc_view.text_area
   28.16            val model = doc_view.model
   28.17            val buffer = model.buffer
   28.18            val snapshot = model.snapshot()
   28.19  
   28.20            if (!snapshot.is_outdated) {
   28.21 -            id match {
   28.22 -              case None =>
   28.23 -                doc_view.text_area.setSelectedText(text)
   28.24 -              case Some(exec_id) =>
   28.25 +            props match {
   28.26 +              case Position.Id(exec_id) =>
   28.27                  snapshot.state.execs.get(exec_id).map(_.command) match {
   28.28                    case Some(command) =>
   28.29                      snapshot.node.command_start(command) match {
   28.30 @@ -42,6 +41,22 @@
   28.31                      }
   28.32                    case None =>
   28.33                  }
   28.34 +              case _ =>
   28.35 +                JEdit_Lib.buffer_edit(buffer) {
   28.36 +                  val text1 =
   28.37 +                    if (props.exists(_ == Markup.PADDING_LINE) &&
   28.38 +                        text_area.getSelectionCount == 0)
   28.39 +                    {
   28.40 +                      def pad(range: Text.Range): String =
   28.41 +                        if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
   28.42 +
   28.43 +                      val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
   28.44 +                      val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
   28.45 +                      pad(before_caret) + text + pad(caret)
   28.46 +                    }
   28.47 +                    else text
   28.48 +                  text_area.setSelectedText(text1)
   28.49 +                }
   28.50              }
   28.51            }
   28.52          }
    29.1 --- a/src/Tools/jEdit/src/token_markup.scala	Mon Nov 26 16:01:04 2012 +0100
    29.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Mon Nov 26 17:13:44 2012 +0100
    29.3 @@ -48,13 +48,7 @@
    29.4      val buffer = text_area.getBuffer
    29.5  
    29.6      text_area.getSelection.toList match {
    29.7 -      case Nil if control == "" =>
    29.8 -        JEdit_Lib.buffer_edit(buffer) {
    29.9 -          val caret = text_area.getCaretPosition
   29.10 -          if (caret > 0 && is_control_style(buffer.getText(caret - 1, 1)))
   29.11 -            text_area.backspace()
   29.12 -        }
   29.13 -      case Nil if control != "" =>
   29.14 +      case Nil =>
   29.15          text_area.setSelectedText(control)
   29.16        case sels =>
   29.17          JEdit_Lib.buffer_edit(buffer) {