# HG changeset patch # User wenzelm # Date 1353946424 -3600 # Node ID 81a067b188b8cadc505adf4129e3da204e1cac2a # Parent 79773c44e57be020f5f111eb10439081257d1406# Parent ce1f0602f48ee0c02fc5a6d3d4c045a4a714cbcc merged diff -r 79773c44e57b -r 81a067b188b8 NEWS --- 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 *** diff -r 79773c44e57b -r 81a067b188b8 src/Doc/IsarRef/Misc.thy --- 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 \"} \\ @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @@ -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. diff -r 79773c44e57b -r 81a067b188b8 src/Doc/IsarRef/Outer_Syntax.thy --- 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 \"} \\ + @{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \"} \\ + \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 diff -r 79773c44e57b -r 81a067b188b8 src/HOL/BNF/Tools/bnf_wrap.ML --- 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 []) ([], [])) ([], ([], []))) diff -r 79773c44e57b -r 81a067b188b8 src/HOL/Boogie/Tools/boogie_commands.ML --- 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)) diff -r 79773c44e57b -r 81a067b188b8 src/HOL/Import/import_data.ML --- 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 diff -r 79773c44e57b -r 81a067b188b8 src/HOL/Import/import_rule.ML --- 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))) diff -r 79773c44e57b -r 81a067b188b8 src/HOL/Statespace/state_space.ML --- 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))); diff -r 79773c44e57b -r 81a067b188b8 src/HOL/Tools/Lifting/lifting_setup.ML --- 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; diff -r 79773c44e57b -r 81a067b188b8 src/HOL/Tools/Nitpick/nitpick.ML --- 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 () diff -r 79773c44e57b -r 81a067b188b8 src/HOL/Tools/inductive.ML --- 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 _ = diff -r 79773c44e57b -r 81a067b188b8 src/HOL/Tools/recdef.ML --- 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)); diff -r 79773c44e57b -r 81a067b188b8 src/Pure/Isar/isar_syn.ML --- 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 _ = diff -r 79773c44e57b -r 81a067b188b8 src/Pure/Isar/outer_syntax.ML --- 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; diff -r 79773c44e57b -r 81a067b188b8 src/Pure/PIDE/markup.ML --- 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"; diff -r 79773c44e57b -r 81a067b188b8 src/Pure/PIDE/markup.scala --- 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" diff -r 79773c44e57b -r 81a067b188b8 src/Pure/PIDE/sendback.ML --- 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; diff -r 79773c44e57b -r 81a067b188b8 src/Pure/ROOT --- 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" diff -r 79773c44e57b -r 81a067b188b8 src/Pure/ROOT.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 *) diff -r 79773c44e57b -r 81a067b188b8 src/Pure/Tools/find_consts.ML --- 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))); diff -r 79773c44e57b -r 81a067b188b8 src/Pure/Tools/find_theorems.ML --- 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 diff -r 79773c44e57b -r 81a067b188b8 src/Pure/Tools/legacy_xml_syntax.ML --- /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 + ("\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; diff -r 79773c44e57b -r 81a067b188b8 src/Pure/Tools/xml_syntax.ML --- 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 - ("\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; diff -r 79773c44e57b -r 81a067b188b8 src/Tools/jEdit/src/jedit_lib.scala --- 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 = diff -r 79773c44e57b -r 81a067b188b8 src/Tools/jEdit/src/pretty_text_area.scala --- 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) diff -r 79773c44e57b -r 81a067b188b8 src/Tools/jEdit/src/rendering.scala --- 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 } diff -r 79773c44e57b -r 81a067b188b8 src/Tools/jEdit/src/rich_text_area.scala --- 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) diff -r 79773c44e57b -r 81a067b188b8 src/Tools/jEdit/src/sendback.scala --- 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) + } } } } diff -r 79773c44e57b -r 81a067b188b8 src/Tools/jEdit/src/token_markup.scala --- 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) {