# HG changeset patch # User wenzelm # Date 1399668966 -7200 # Node ID 2c664c817bdf80090850a922c03bf0ba6d4119d1 # Parent 40213e24c8c4e76d3e3e6e87bd6217bbb558183b# Parent b47193851dc6993c81241efdea87aa7d675d0229 merged diff -r 40213e24c8c4 -r 2c664c817bdf src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Fri May 09 08:13:37 2014 +0200 +++ b/src/HOL/Tools/Function/function.ML Fri May 09 22:56:06 2014 +0200 @@ -132,7 +132,9 @@ fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases', pelims=pelims',elims=NONE} - val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes) + val _ = + Proof_Display.print_consts do_print (Position.thread_data ()) lthy + (K false) (map fst fixes) in (info, lthy |> Local_Theory.declaration {syntax = false, pervasive = false} diff -r 40213e24c8c4 -r 2c664c817bdf src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Fri May 09 08:13:37 2014 +0200 +++ b/src/Pure/Isar/obtain.ML Fri May 09 22:56:06 2014 +0200 @@ -299,8 +299,9 @@ end; val goal = Var (("guess", 0), propT); + val pos = Position.thread_data (); fun print_result ctxt' (k, [(s, [_, th])]) = - Proof_Display.print_results int ctxt' (k, [(s, [th])]); + Proof_Display.print_results int pos ctxt' (k, [(s, [th])]); val before_qed = Method.primitive_text (fn ctxt => Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #> diff -r 40213e24c8c4 -r 2c664c817bdf src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri May 09 08:13:37 2014 +0200 +++ b/src/Pure/Isar/proof.ML Fri May 09 22:56:06 2014 +0200 @@ -1045,7 +1045,7 @@ local fun gen_have prep_att prepp before_qed after_qed stmt int = - local_goal (Proof_Display.print_results int) + local_goal (Proof_Display.print_results int (Position.thread_data ())) prep_att prepp "have" before_qed after_qed stmt; fun gen_show prep_att prepp before_qed after_qed stmt int state = @@ -1057,13 +1057,17 @@ (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th]) |> cat_lines; + val pos = Position.thread_data (); fun print_results ctxt res = if ! testing then () - else Proof_Display.print_results int ctxt res; + else Proof_Display.print_results int pos ctxt res; fun print_rule ctxt th = if ! testing then rule := SOME th else if int then - writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th)) + Proof_Display.string_of_rule ctxt "Successful" th + |> Markup.markup Markup.text_fold + |> Markup.markup Markup.state + |> writeln else (); val test_proof = local_skip_proof true diff -r 40213e24c8c4 -r 2c664c817bdf src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Fri May 09 08:13:37 2014 +0200 +++ b/src/Pure/Isar/proof_display.ML Fri May 09 22:56:06 2014 +0200 @@ -22,8 +22,10 @@ val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T val method_error: string -> Position.T -> {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result - val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit - val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit + val print_results: bool -> Position.T -> Proof.context -> + ((string * string) * (string * thm list) list) -> unit + val print_consts: bool -> Position.T -> Proof.context -> + (string * typ -> bool) -> (string * typ) list -> unit end structure Proof_Display: PROOF_DISPLAY = @@ -127,11 +129,13 @@ (* results *) +fun position_markup pos = Pretty.mark (Position.markup pos Markup.position); + local -fun pretty_fact_name (kind, "") = Pretty.keyword1 kind - | pretty_fact_name (kind, name) = - Pretty.block [Pretty.keyword1 kind, Pretty.brk 1, +fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind) + | pretty_fact_name pos (kind, name) = + Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1, Pretty.str (Long_Name.base_name name), Pretty.str ":"]; fun pretty_facts ctxt = @@ -140,17 +144,18 @@ in -fun print_results do_print ctxt ((kind, name), facts) = +fun print_results do_print pos ctxt ((kind, name), facts) = if not do_print orelse kind = "" then () else if name = "" then (Pretty.writeln o Pretty.mark Markup.state) - (Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts)) + (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 :: + pretty_facts ctxt facts)) else (Pretty.writeln o Pretty.mark Markup.state) (case facts of - [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk, + [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk, Proof_Context.pretty_fact ctxt fact]) - | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk, + | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk, Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])); end; @@ -164,18 +169,19 @@ Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)]; -fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs); +fun pretty_vars pos ctxt kind vs = + Pretty.block (Pretty.fbreaks (position_markup pos (Pretty.str kind) :: map (pretty_var ctxt) vs)); -fun pretty_consts ctxt pred cs = +fun pretty_consts pos ctxt pred cs = (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of - [] => pretty_vars ctxt "constants" cs - | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]); + [] => pretty_vars pos ctxt "constants" cs + | ps => Pretty.chunks [pretty_vars pos ctxt "parameters" ps, pretty_vars pos ctxt "constants" cs]); in -fun print_consts do_print ctxt pred cs = +fun print_consts do_print pos ctxt pred cs = if not do_print orelse null cs then () - else Pretty.writeln (Pretty.mark Markup.state (pretty_consts ctxt pred cs)); + else Pretty.writeln (Pretty.mark Markup.state (pretty_consts pos ctxt pred cs)); end; diff -r 40213e24c8c4 -r 2c664c817bdf src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri May 09 08:13:37 2014 +0200 +++ b/src/Pure/Isar/specification.ML Fri May 09 22:56:06 2014 +0200 @@ -223,7 +223,9 @@ val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs; - val _ = Proof_Display.print_consts int lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)]; + val _ = + Proof_Display.print_consts int (Position.thread_data ()) lthy4 + (member (op =) (Term.add_frees lhs' [])) [(x, T)]; in ((lhs, (def_name, th')), lthy4) end; val definition' = gen_def check_free_spec; @@ -256,7 +258,7 @@ |> Local_Theory.abbrev mode (var, rhs) |> snd |> Proof_Context.restore_syntax_mode lthy; - val _ = Proof_Display.print_consts int lthy2 (K false) [(x, T)]; + val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)]; in lthy2 end; val abbreviation = gen_abbrev check_free_spec; @@ -301,7 +303,7 @@ |> Attrib.partial_evaluation ctxt' |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy); val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts'; - val _ = Proof_Display.print_results int lthy' ((kind, ""), res); + val _ = Proof_Display.print_results int (Position.thread_data ()) lthy' ((kind, ""), res); in (res, lthy') end; in @@ -389,6 +391,7 @@ |> prep_statement (prep_att lthy) prep_stmt elems raw_concl; val atts = more_atts @ map (prep_att lthy) raw_atts; + val pos = Position.thread_data (); fun after_qed' results goal_ctxt' = let val results' = @@ -400,12 +403,12 @@ (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy; val lthy'' = if Attrib.is_empty_binding (name, atts) then - (Proof_Display.print_results int lthy' ((kind, ""), res); lthy') + (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy') else let val ([(res_name, _)], lthy'') = Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy'; - val _ = Proof_Display.print_results int lthy' ((kind, res_name), res); + val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res); in lthy'' end; in after_qed results' lthy'' end; in diff -r 40213e24c8c4 -r 2c664c817bdf src/Tools/jEdit/src/dockable.scala --- a/src/Tools/jEdit/src/dockable.scala Fri May 09 08:13:37 2014 +0200 +++ b/src/Tools/jEdit/src/dockable.scala Fri May 09 22:56:06 2014 +0200 @@ -22,7 +22,7 @@ if (position == DockableWindowManager.FLOATING) setPreferredSize(new Dimension(500, 250)) - def focusOnDefaultComponent { requestFocus } + def focusOnDefaultComponent { JEdit_Lib.request_focus_view(view) } def set_content(c: Component) { add(c, BorderLayout.CENTER) } def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) } diff -r 40213e24c8c4 -r 2c664c817bdf src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Fri May 09 08:13:37 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Fri May 09 22:56:06 2014 +0200 @@ -326,9 +326,9 @@ /* key event handling */ - def request_focus_view + def request_focus_view(alt_view: View = null) { - val view = jEdit.getActiveView() + val view = if (alt_view != null) alt_view else jEdit.getActiveView() if (view != null) { val text_area = view.getTextArea if (text_area != null) text_area.requestFocus diff -r 40213e24c8c4 -r 2c664c817bdf src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Fri May 09 08:13:37 2014 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Fri May 09 22:56:06 2014 +0200 @@ -20,9 +20,6 @@ class Output_Dockable(view: View, position: String) extends Dockable(view, position) { - override def focusOnDefaultComponent { view.getTextArea.requestFocus } - - /* component state -- owned by Swing thread */ private var zoom_factor = 100 diff -r 40213e24c8c4 -r 2c664c817bdf src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Fri May 09 08:13:37 2014 +0200 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri May 09 22:56:06 2014 +0200 @@ -136,7 +136,7 @@ case Some((old, _ :: rest)) => rest match { case top :: _ => top.request_focus - case Nil => JEdit_Lib.request_focus_view + case Nil => JEdit_Lib.request_focus_view() } old.foreach(_.hide_popup) tip.hide_popup @@ -153,7 +153,7 @@ deactivate() if (stack.isEmpty) false else { - JEdit_Lib.request_focus_view + JEdit_Lib.request_focus_view() stack.foreach(_.hide_popup) stack = Nil true