--- a/NEWS Mon Nov 26 16:01:04 2012 +0100
+++ b/NEWS Mon Nov 26 17:13:44 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 16:01:04 2012 +0100
+++ b/src/Doc/IsarRef/Misc.thy Mon Nov 26 17:13:44 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 16:01:04 2012 +0100
+++ b/src/Doc/IsarRef/Outer_Syntax.thy Mon Nov 26 17:13:44 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/HOL/BNF/Tools/bnf_wrap.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML Mon Nov 26 17:13:44 2012 +0100
@@ -675,7 +675,7 @@
>> (pairself (exists I) o split_list)) (false, false);
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"
+ Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wrap an existing datatype"
((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon Nov 26 17:13:44 2012 +0100
@@ -302,7 +302,7 @@
val _ =
Outer_Syntax.command @{command_spec "boogie_vc"}
- "enter into proof mode for a specific verification condition"
+ "enter into proof mode for a specific Boogie verification condition"
(vc_name -- vc_opts >> (fn args =>
(Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
@@ -334,7 +334,7 @@
val _ =
Outer_Syntax.improper_command @{command_spec "boogie_status"}
- "show the name and state of all loaded verification conditions"
+ "show the name and state of all loaded Boogie verification conditions"
(status_test >> status_cmd ||
status_vc >> status_cmd ||
Scan.succeed (status_cmd boogie_status))
--- a/src/HOL/Import/import_data.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/HOL/Import/import_data.ML Mon Nov 26 17:13:44 2012 +0100
@@ -104,13 +104,13 @@
val type_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
(fn (ty_name1, ty_name2) => add_typ_map ty_name1 ty_name2)
val _ = Outer_Syntax.command @{command_spec "import_type_map"}
- "Map external type name to existing Isabelle/HOL type name"
+ "map external type name to existing Isabelle/HOL type name"
(type_map >> Toplevel.theory)
val const_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
(fn (cname1, cname2) => add_const_map cname1 cname2)
val _ = Outer_Syntax.command @{command_spec "import_const_map"}
- "Map external const name to existing Isabelle/HOL const name"
+ "map external const name to existing Isabelle/HOL const name"
(const_map >> Toplevel.theory)
(* Initial type and constant maps, for types and constants that are not
--- a/src/HOL/Import/import_rule.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/HOL/Import/import_rule.ML Mon Nov 26 17:13:44 2012 +0100
@@ -443,7 +443,7 @@
(thy, init_state) |> File.fold_lines process_line path |> fst
val _ = Outer_Syntax.command @{command_spec "import_file"}
- "Import a recorded proof file"
+ "import a recorded proof file"
(Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
--- a/src/HOL/Statespace/state_space.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/HOL/Statespace/state_space.ML Mon Nov 26 17:13:44 2012 +0100
@@ -706,7 +706,7 @@
(plus1_unless comp parent --
Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
val _ =
- Outer_Syntax.command @{command_spec "statespace"} "define state space"
+ Outer_Syntax.command @{command_spec "statespace"} "define state-space as locale context"
(statespace_decl >> (fn ((args, name), (parents, comps)) =>
Toplevel.theory (define_statespace args name parents comps)));
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Nov 26 17:13:44 2012 +0100
@@ -309,7 +309,7 @@
val _ =
Outer_Syntax.local_theory @{command_spec "setup_lifting"}
- "Setup lifting infrastructure"
+ "setup lifting infrastructure"
(opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >>
(fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm))
end;
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 26 17:13:44 2012 +0100
@@ -470,7 +470,8 @@
pprint_nt (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
\general enough, try this command: " @
- [Pretty.mark (Sendback.make_markup ()) (Pretty.blk (0,
+ [Pretty.mark (Sendback.make_markup {implicit = false, properties = []})
+ (Pretty.blk (0,
pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
else
()
--- a/src/HOL/Tools/inductive.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/HOL/Tools/inductive.ML Mon Nov 26 17:13:44 2012 +0100
@@ -1157,7 +1157,7 @@
val _ =
Outer_Syntax.local_theory @{command_spec "inductive_cases"}
- "create simplified instances of elimination rules (improper)"
+ "create simplified instances of elimination rules"
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
val _ =
--- a/src/HOL/Tools/recdef.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/HOL/Tools/recdef.ML Mon Nov 26 17:13:44 2012 +0100
@@ -302,7 +302,7 @@
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
val _ =
- Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (TFL)"
+ Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)"
(recdef_decl >> Toplevel.theory);
@@ -314,12 +314,12 @@
val _ =
Outer_Syntax.command @{command_spec "defer_recdef"}
- "defer general recursive functions (TFL)"
+ "defer general recursive functions (obsolete TFL)"
(defer_recdef_decl >> Toplevel.theory);
val _ =
Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
- "recommence proof of termination condition (TFL)"
+ "recommence proof of termination condition (obsolete TFL)"
((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
>> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
--- a/src/Pure/Isar/isar_syn.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Nov 26 17:13:44 2012 +0100
@@ -134,11 +134,11 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
val _ =
- Outer_Syntax.command @{command_spec "syntax"} "declare syntactic constants"
+ Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
(opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
val _ =
- Outer_Syntax.command @{command_spec "no_syntax"} "delete syntax declarations"
+ Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
(opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
@@ -159,11 +159,11 @@
>> (fn (left, (arr, right)) => arr (left, right));
val _ =
- Outer_Syntax.command @{command_spec "translations"} "declare syntax translation rules"
+ Outer_Syntax.command @{command_spec "translations"} "add syntax translation rules"
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
val _ =
- Outer_Syntax.command @{command_spec "no_translations"} "remove syntax translation rules"
+ Outer_Syntax.command @{command_spec "no_translations"} "delete syntax translation rules"
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
@@ -538,7 +538,7 @@
(Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
val _ =
- Outer_Syntax.command @{command_spec "hence"} "abbreviates \"then have\""
+ Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
(Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
val _ =
@@ -547,7 +547,7 @@
(Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
val _ =
- Outer_Syntax.command @{command_spec "thus"} "abbreviates \"then show\""
+ Outer_Syntax.command @{command_spec "thus"} "old-style alias of \"then show\""
(Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
@@ -595,7 +595,7 @@
(Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
val _ =
- Outer_Syntax.command @{command_spec "def"} "local definition"
+ Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
(Parse.and_list1
(Parse_Spec.opt_thm_name ":" --
((Parse.binding -- Parse.opt_mixfix) --
@@ -649,7 +649,7 @@
(* end proof *)
val _ =
- Outer_Syntax.command @{command_spec "qed"} "conclude (sub-)proof"
+ Outer_Syntax.command @{command_spec "qed"} "conclude proof"
(Scan.option Method.parse >> Isar_Cmd.qed);
val _ =
@@ -692,11 +692,11 @@
(Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
val _ =
- Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement (unstructured)"
+ Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
(Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
val _ =
- Outer_Syntax.command @{command_spec "proof"} "backward proof"
+ Outer_Syntax.command @{command_spec "proof"} "backward proof step"
(Scan.option Method.parse >> (fn m => Toplevel.print o
Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
Toplevel.skip_proof (fn i => i + 1)));
@@ -741,7 +741,7 @@
(Position.of_properties (Position.default_properties pos props), str));
val _ =
- Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "nested Isabelle command"
+ Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command"
(props_text :|-- (fn (pos, str) =>
(case Outer_Syntax.parse pos str of
[tr] => Scan.succeed (K tr)
@@ -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"
@@ -849,8 +851,7 @@
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_antiquotations"}
- "print antiquotations (global)"
+ Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
val _ =
@@ -984,7 +985,7 @@
val _ =
Outer_Syntax.improper_command @{command_spec "commit"}
- "commit current session to ML database"
+ "commit current session to ML session image"
(Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
val _ =
--- a/src/Pure/Isar/outer_syntax.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Mon Nov 26 17:13:44 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, properties = [Markup.padding_line]},
+ 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;
--- a/src/Pure/PIDE/markup.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Nov 26 17:13:44 2012 +0100
@@ -96,6 +96,8 @@
val proof_stateN: string val proof_state: int -> T
val stateN: string val state: T
val subgoalN: string val subgoal: T
+ val paddingN: string
+ val padding_line: string * string
val sendbackN: string val sendback: T
val intensifyN: string val intensify: T
val taskN: string
@@ -333,7 +335,11 @@
val (stateN, state) = markup_elem "state";
val (subgoalN, subgoal) = markup_elem "subgoal";
+
+val paddingN = "padding";
+val padding_line = (paddingN, lineN);
val (sendbackN, sendback) = markup_elem "sendback";
+
val (intensifyN, intensify) = markup_elem "intensify";
--- a/src/Pure/PIDE/markup.scala Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Pure/PIDE/markup.scala Mon Nov 26 17:13:44 2012 +0100
@@ -211,7 +211,11 @@
val STATE = "state"
val SUBGOAL = "subgoal"
+
+ val PADDING = "padding"
+ val PADDING_LINE = (PADDING, LINE)
val SENDBACK = "sendback"
+
val INTENSIFY = "intensify"
--- a/src/Pure/PIDE/sendback.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Pure/PIDE/sendback.ML Mon Nov 26 17:13:44 2012 +0100
@@ -7,25 +7,27 @@
signature SENDBACK =
sig
- val make_markup: unit -> Markup.T
+ val make_markup: {implicit: bool, properties: Properties.T} -> Markup.T
+ val markup_implicit: string -> string
val markup: string -> string
- val markup_implicit: string -> string
end;
structure Sendback: SENDBACK =
struct
-fun make_markup () =
- let
- val props =
- (case Position.get_id (Position.thread_data ()) of
- SOME id => [(Markup.idN, id)]
- | NONE => []);
- in Markup.properties props Markup.sendback end;
+fun make_markup {implicit, properties} =
+ Markup.sendback
+ |> not implicit ? (fn markup =>
+ let
+ val props =
+ (case Position.get_id (Position.thread_data ()) of
+ SOME id => [(Markup.idN, id)]
+ | NONE => []);
+ in Markup.properties props markup end)
+ |> Markup.properties properties;
-fun markup s = Markup.markup (make_markup ()) s;
-
-fun markup_implicit s = Markup.markup Markup.sendback s;
+fun markup_implicit s = Markup.markup (make_markup {implicit = true, properties = []}) s;
+fun markup s = Markup.markup (make_markup {implicit = false, properties = []}) s;
end;
--- a/src/Pure/ROOT Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Pure/ROOT Mon Nov 26 17:13:44 2012 +0100
@@ -200,7 +200,7 @@
"Thy/thy_output.ML"
"Thy/thy_syntax.ML"
"Tools/named_thms.ML"
- "Tools/xml_syntax.ML"
+ "Tools/legacy_xml_syntax.ML"
"assumption.ML"
"axclass.ML"
"config.ML"
--- a/src/Pure/ROOT.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Pure/ROOT.ML Mon Nov 26 17:13:44 2012 +0100
@@ -283,7 +283,7 @@
use "Tools/named_thms.ML";
-use "Tools/xml_syntax.ML";
+use "Tools/legacy_xml_syntax.ML";
(* configuration for Proof General *)
--- a/src/Pure/Tools/find_consts.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Pure/Tools/find_consts.ML Mon Nov 26 17:13:44 2012 +0100
@@ -136,7 +136,8 @@
in
val _ =
- Outer_Syntax.improper_command @{command_spec "find_consts"} "search constants by type pattern"
+ Outer_Syntax.improper_command @{command_spec "find_consts"}
+ "find constants by name/type patterns"
(Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
>> (fn spec => Toplevel.no_timing o
Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
--- a/src/Pure/Tools/find_theorems.ML Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Pure/Tools/find_theorems.ML Mon Nov 26 17:13:44 2012 +0100
@@ -116,17 +116,17 @@
| xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
| xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
| xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
- | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []) , [XML_Syntax.xml_of_term pat])
- | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []) , [XML_Syntax.xml_of_term pat]);
+ | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []), [Legacy_XML_Syntax.xml_of_term pat])
+ | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []), [Legacy_XML_Syntax.xml_of_term pat]);
fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
| criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
| criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
| criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
| criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
- | criterion_of_xml (XML.Elem (("Simp", []) , [tree])) = Simp (XML_Syntax.term_of_xml tree)
- | criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
- | criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
+ | criterion_of_xml (XML.Elem (("Simp", []), [tree])) = Simp (Legacy_XML_Syntax.term_of_xml tree)
+ | criterion_of_xml (XML.Elem (("Pattern", []), [tree])) = Pattern (Legacy_XML_Syntax.term_of_xml tree)
+ | criterion_of_xml tree = raise Legacy_XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
let
@@ -149,7 +149,7 @@
in
{goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
end
- | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
+ | query_of_xml tree = raise Legacy_XML_Syntax.XML ("query_of_xml: bad tree", tree);
@@ -167,7 +167,7 @@
fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
| xml_of_theorem (External (fact_ref, prop)) =
- XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop]);
+ XML.Elem (fact_ref_markup fact_ref ("External", []), [Legacy_XML_Syntax.xml_of_term prop]);
fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
let
@@ -177,9 +177,9 @@
Option.map (single o Facts.Single o Markup.parse_int)
(Properties.get properties "index");
in
- External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
+ External (Facts.Named ((name, pos), intvs_opt), Legacy_XML_Syntax.term_of_xml tree)
end
- | theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
+ | theorem_of_xml tree = raise Legacy_XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
fun xml_of_result (opt_found, theorems) =
let
@@ -192,7 +192,7 @@
fun result_of_xml (XML.Elem (("Result", properties), body)) =
(Properties.get properties "found" |> Option.map Markup.parse_int,
XML.Decode.list (theorem_of_xml o the_single) body)
- | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
+ | result_of_xml tree = raise Legacy_XML_Syntax.XML ("result_of_xml: bad tree", tree);
fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
| prop_of (External (_, prop)) = prop;
@@ -625,7 +625,7 @@
val _ =
Outer_Syntax.improper_command @{command_spec "find_theorems"}
- "print theorems meeting specified criteria"
+ "find theorems meeting specified criteria"
(options -- query_parser
>> (fn ((opt_lim, rem_dups), spec) =>
Toplevel.no_timing o
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/legacy_xml_syntax.ML Mon Nov 26 17:13:44 2012 +0100
@@ -0,0 +1,173 @@
+(* Title: Pure/Tools/legacy_xml_syntax.ML
+ Author: Stefan Berghofer, TU Muenchen
+
+Input and output of types, terms, and proofs in XML format.
+See isabelle.xsd for a description of the syntax.
+
+Legacy module, see Pure/term_xml.ML etc.
+*)
+
+signature LEGACY_XML_SYNTAX =
+sig
+ val xml_of_type: typ -> XML.tree
+ val xml_of_term: term -> XML.tree
+ val xml_of_proof: Proofterm.proof -> XML.tree
+ val write_to_file: Path.T -> string -> XML.tree -> unit
+ exception XML of string * XML.tree
+ val type_of_xml: XML.tree -> typ
+ val term_of_xml: XML.tree -> term
+ val proof_of_xml: XML.tree -> Proofterm.proof
+end;
+
+structure Legacy_XML_Syntax : LEGACY_XML_SYNTAX =
+struct
+
+(**** XML output ****)
+
+fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
+
+fun xml_of_type (TVar ((s, i), S)) =
+ XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
+ map xml_of_class S)
+ | xml_of_type (TFree (s, S)) =
+ XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
+ | xml_of_type (Type (s, Ts)) =
+ XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
+
+fun xml_of_term (Bound i) =
+ XML.Elem (("Bound", [("index", string_of_int i)]), [])
+ | xml_of_term (Free (s, T)) =
+ XML.Elem (("Free", [("name", s)]), [xml_of_type T])
+ | xml_of_term (Var ((s, i), T)) =
+ XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
+ [xml_of_type T])
+ | xml_of_term (Const (s, T)) =
+ XML.Elem (("Const", [("name", s)]), [xml_of_type T])
+ | xml_of_term (t $ u) =
+ XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
+ | xml_of_term (Abs (s, T, t)) =
+ XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
+
+fun xml_of_opttypes NONE = []
+ | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
+
+(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
+(* it can be looked up in the theorem database. Thus, it could be *)
+(* omitted from the xml representation. *)
+
+(* FIXME not exhaustive *)
+fun xml_of_proof (PBound i) =
+ XML.Elem (("PBound", [("index", string_of_int i)]), [])
+ | xml_of_proof (Abst (s, optT, prf)) =
+ XML.Elem (("Abst", [("vname", s)]),
+ (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
+ | xml_of_proof (AbsP (s, optt, prf)) =
+ XML.Elem (("AbsP", [("vname", s)]),
+ (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
+ | xml_of_proof (prf % optt) =
+ XML.Elem (("Appt", []),
+ xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
+ | xml_of_proof (prf %% prf') =
+ XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
+ | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
+ | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
+ XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
+ | xml_of_proof (PAxm (s, t, optTs)) =
+ XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
+ | xml_of_proof (Oracle (s, t, optTs)) =
+ XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
+ | xml_of_proof MinProof =
+ XML.Elem (("MinProof", []), []);
+
+
+(* useful for checking the output against a schema file *)
+
+fun write_to_file path elname x =
+ File.write path
+ ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
+ XML.string_of (XML.Elem ((elname,
+ [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
+ ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
+ [x])));
+
+
+
+(**** XML input ****)
+
+exception XML of string * XML.tree;
+
+fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
+ | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
+
+fun index_of_string s tree idx =
+ (case Int.fromString idx of
+ NONE => raise XML (s ^ ": bad index", tree)
+ | SOME i => i);
+
+fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
+ ((case Properties.get atts "name" of
+ NONE => raise XML ("type_of_xml: name of TVar missing", tree)
+ | SOME name => name,
+ the_default 0 (Option.map (index_of_string "type_of_xml" tree)
+ (Properties.get atts "index"))),
+ map class_of_xml classes)
+ | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
+ TFree (s, map class_of_xml classes)
+ | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
+ Type (s, map type_of_xml types)
+ | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
+
+fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
+ Bound (index_of_string "bad variable index" tree idx)
+ | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
+ Free (s, type_of_xml typ)
+ | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
+ ((case Properties.get atts "name" of
+ NONE => raise XML ("type_of_xml: name of Var missing", tree)
+ | SOME name => name,
+ the_default 0 (Option.map (index_of_string "term_of_xml" tree)
+ (Properties.get atts "index"))),
+ type_of_xml typ)
+ | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
+ Const (s, type_of_xml typ)
+ | term_of_xml (XML.Elem (("App", []), [term, term'])) =
+ term_of_xml term $ term_of_xml term'
+ | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
+ Abs (s, type_of_xml typ, term_of_xml term)
+ | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
+
+fun opttypes_of_xml [] = NONE
+ | opttypes_of_xml [XML.Elem (("types", []), types)] =
+ SOME (map type_of_xml types)
+ | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
+
+fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
+ PBound (index_of_string "proof_of_xml" tree idx)
+ | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
+ Abst (s, NONE, proof_of_xml proof)
+ | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
+ Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
+ | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
+ AbsP (s, NONE, proof_of_xml proof)
+ | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
+ AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
+ | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
+ proof_of_xml proof % NONE
+ | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
+ proof_of_xml proof % SOME (term_of_xml term)
+ | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
+ proof_of_xml proof %% proof_of_xml proof'
+ | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
+ Hyp (term_of_xml term)
+ | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
+ (* FIXME? *)
+ PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
+ Future.value (Proofterm.approximate_proof_body MinProof)))
+ | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
+ PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
+ | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
+ Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
+ | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
+ | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
+
+end;
--- a/src/Pure/Tools/xml_syntax.ML Mon Nov 26 16:01:04 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-(* Title: Pure/Tools/xml_syntax.ML
- Author: Stefan Berghofer, TU Muenchen
-
-Input and output of types, terms, and proofs in XML format.
-See isabelle.xsd for a description of the syntax.
-*)
-
-signature XML_SYNTAX =
-sig
- val xml_of_type: typ -> XML.tree
- val xml_of_term: term -> XML.tree
- val xml_of_proof: Proofterm.proof -> XML.tree
- val write_to_file: Path.T -> string -> XML.tree -> unit
- exception XML of string * XML.tree
- val type_of_xml: XML.tree -> typ
- val term_of_xml: XML.tree -> term
- val proof_of_xml: XML.tree -> Proofterm.proof
-end;
-
-structure XML_Syntax : XML_SYNTAX =
-struct
-
-(**** XML output ****)
-
-fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
-
-fun xml_of_type (TVar ((s, i), S)) =
- XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
- map xml_of_class S)
- | xml_of_type (TFree (s, S)) =
- XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
- | xml_of_type (Type (s, Ts)) =
- XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
-
-fun xml_of_term (Bound i) =
- XML.Elem (("Bound", [("index", string_of_int i)]), [])
- | xml_of_term (Free (s, T)) =
- XML.Elem (("Free", [("name", s)]), [xml_of_type T])
- | xml_of_term (Var ((s, i), T)) =
- XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
- [xml_of_type T])
- | xml_of_term (Const (s, T)) =
- XML.Elem (("Const", [("name", s)]), [xml_of_type T])
- | xml_of_term (t $ u) =
- XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
- | xml_of_term (Abs (s, T, t)) =
- XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
-
-fun xml_of_opttypes NONE = []
- | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
-
-(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
-(* it can be looked up in the theorem database. Thus, it could be *)
-(* omitted from the xml representation. *)
-
-(* FIXME not exhaustive *)
-fun xml_of_proof (PBound i) =
- XML.Elem (("PBound", [("index", string_of_int i)]), [])
- | xml_of_proof (Abst (s, optT, prf)) =
- XML.Elem (("Abst", [("vname", s)]),
- (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
- | xml_of_proof (AbsP (s, optt, prf)) =
- XML.Elem (("AbsP", [("vname", s)]),
- (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
- | xml_of_proof (prf % optt) =
- XML.Elem (("Appt", []),
- xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
- | xml_of_proof (prf %% prf') =
- XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
- | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
- | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
- XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
- | xml_of_proof (PAxm (s, t, optTs)) =
- XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
- | xml_of_proof (Oracle (s, t, optTs)) =
- XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
- | xml_of_proof MinProof =
- XML.Elem (("MinProof", []), []);
-
-
-(* useful for checking the output against a schema file *)
-
-fun write_to_file path elname x =
- File.write path
- ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
- XML.string_of (XML.Elem ((elname,
- [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
- ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
- [x])));
-
-
-
-(**** XML input ****)
-
-exception XML of string * XML.tree;
-
-fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
- | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
-
-fun index_of_string s tree idx =
- (case Int.fromString idx of
- NONE => raise XML (s ^ ": bad index", tree)
- | SOME i => i);
-
-fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
- ((case Properties.get atts "name" of
- NONE => raise XML ("type_of_xml: name of TVar missing", tree)
- | SOME name => name,
- the_default 0 (Option.map (index_of_string "type_of_xml" tree)
- (Properties.get atts "index"))),
- map class_of_xml classes)
- | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
- TFree (s, map class_of_xml classes)
- | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
- Type (s, map type_of_xml types)
- | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
-
-fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
- Bound (index_of_string "bad variable index" tree idx)
- | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
- Free (s, type_of_xml typ)
- | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
- ((case Properties.get atts "name" of
- NONE => raise XML ("type_of_xml: name of Var missing", tree)
- | SOME name => name,
- the_default 0 (Option.map (index_of_string "term_of_xml" tree)
- (Properties.get atts "index"))),
- type_of_xml typ)
- | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
- Const (s, type_of_xml typ)
- | term_of_xml (XML.Elem (("App", []), [term, term'])) =
- term_of_xml term $ term_of_xml term'
- | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
- Abs (s, type_of_xml typ, term_of_xml term)
- | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
-
-fun opttypes_of_xml [] = NONE
- | opttypes_of_xml [XML.Elem (("types", []), types)] =
- SOME (map type_of_xml types)
- | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
-
-fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
- PBound (index_of_string "proof_of_xml" tree idx)
- | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
- Abst (s, NONE, proof_of_xml proof)
- | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
- Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
- | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
- AbsP (s, NONE, proof_of_xml proof)
- | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
- AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
- | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
- proof_of_xml proof % NONE
- | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
- proof_of_xml proof % SOME (term_of_xml term)
- | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
- proof_of_xml proof %% proof_of_xml proof'
- | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
- Hyp (term_of_xml term)
- | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
- (* FIXME? *)
- PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
- Future.value (Proofterm.approximate_proof_body MinProof)))
- | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
- PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
- | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
- Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
- | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
- | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
-
-end;
--- a/src/Tools/jEdit/src/jedit_lib.scala Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Nov 26 17:13:44 2012 +0100
@@ -105,6 +105,13 @@
}
+ /* get text */
+
+ def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
+ try { Some(buffer.getText(range.start, range.length)) }
+ catch { case _: ArrayIndexOutOfBoundsException => None }
+
+
/* point range */
def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
--- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Nov 26 17:13:44 2012 +0100
@@ -93,6 +93,7 @@
Swing_Thread.later {
current_rendering = rendering
JEdit_Lib.buffer_edit(getBuffer) {
+ rich_text_area.active_reset()
getBuffer.setReadOnly(false)
setText(text)
setCaretPosition(0)
--- a/src/Tools/jEdit/src/rendering.scala Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Mon Nov 26 17:13:44 2012 +0100
@@ -249,11 +249,11 @@
}
- def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
+ def sendback(range: Text.Range): Option[Text.Info[Properties.T]] =
snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
{
case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
- Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
+ Text.Info(snapshot.convert(info_range), props)
}) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Nov 26 17:13:44 2012 +0100
@@ -134,11 +134,11 @@
private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
- private val sendback_area = new Active_Area[Option[Document.Exec_ID]]((r: Rendering) => r.sendback _)
+ private val sendback_area = new Active_Area[Properties.T]((r: Rendering) => r.sendback _)
private val active_areas =
List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
- private def active_reset(): Unit = active_areas.foreach(_._1.reset)
+ def active_reset(): Unit = active_areas.foreach(_._1.reset)
private val focus_listener = new FocusAdapter {
override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
@@ -157,7 +157,7 @@
case None =>
}
sendback_area.text_info match {
- case Some((text, Text.Info(_, id))) => Sendback.activate(view, text, id)
+ case Some((text, Text.Info(_, props))) => Sendback.activate(view, text, props)
case None =>
}
}
@@ -172,7 +172,7 @@
if ((control || hovering) && !buffer.isLoading) {
JEdit_Lib.buffer_lock(buffer) {
JEdit_Lib.pixel_range(text_area, e.getX(), e.getY()) match {
- case None =>
+ case None => active_reset()
case Some(range) =>
val rendering = get_rendering()
for ((area, require_control) <- active_areas)
--- a/src/Tools/jEdit/src/sendback.scala Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Tools/jEdit/src/sendback.scala Mon Nov 26 17:13:44 2012 +0100
@@ -14,22 +14,21 @@
object Sendback
{
- def activate(view: View, text: String, id: Option[Document.Exec_ID])
+ def activate(view: View, text: String, props: Properties.T)
{
Swing_Thread.require()
Document_View(view.getTextArea) match {
case Some(doc_view) =>
doc_view.rich_text_area.robust_body() {
+ val text_area = doc_view.text_area
val model = doc_view.model
val buffer = model.buffer
val snapshot = model.snapshot()
if (!snapshot.is_outdated) {
- id match {
- case None =>
- doc_view.text_area.setSelectedText(text)
- case Some(exec_id) =>
+ props match {
+ case Position.Id(exec_id) =>
snapshot.state.execs.get(exec_id).map(_.command) match {
case Some(command) =>
snapshot.node.command_start(command) match {
@@ -42,6 +41,22 @@
}
case None =>
}
+ case _ =>
+ JEdit_Lib.buffer_edit(buffer) {
+ val text1 =
+ if (props.exists(_ == Markup.PADDING_LINE) &&
+ text_area.getSelectionCount == 0)
+ {
+ def pad(range: Text.Range): String =
+ if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
+
+ val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
+ val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
+ pad(before_caret) + text + pad(caret)
+ }
+ else text
+ text_area.setSelectedText(text1)
+ }
}
}
}
--- a/src/Tools/jEdit/src/token_markup.scala Mon Nov 26 16:01:04 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Mon Nov 26 17:13:44 2012 +0100
@@ -48,13 +48,7 @@
val buffer = text_area.getBuffer
text_area.getSelection.toList match {
- case Nil if control == "" =>
- JEdit_Lib.buffer_edit(buffer) {
- val caret = text_area.getCaretPosition
- if (caret > 0 && is_control_style(buffer.getText(caret - 1, 1)))
- text_area.backspace()
- }
- case Nil if control != "" =>
+ case Nil =>
text_area.setSelectedText(control)
case sels =>
JEdit_Lib.buffer_edit(buffer) {