--- 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}
--- 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 #>
--- 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
--- 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;
--- 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
--- 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) }
--- 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
--- 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
--- 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