1.1 --- a/src/HOL/Tools/Function/function.ML Fri May 09 08:13:37 2014 +0200
1.2 +++ b/src/HOL/Tools/Function/function.ML Fri May 09 22:56:06 2014 +0200
1.3 @@ -132,7 +132,9 @@
1.4 fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
1.5 pelims=pelims',elims=NONE}
1.6
1.7 - val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
1.8 + val _ =
1.9 + Proof_Display.print_consts do_print (Position.thread_data ()) lthy
1.10 + (K false) (map fst fixes)
1.11 in
1.12 (info,
1.13 lthy |> Local_Theory.declaration {syntax = false, pervasive = false}
2.1 --- a/src/Pure/Isar/obtain.ML Fri May 09 08:13:37 2014 +0200
2.2 +++ b/src/Pure/Isar/obtain.ML Fri May 09 22:56:06 2014 +0200
2.3 @@ -299,8 +299,9 @@
2.4 end;
2.5
2.6 val goal = Var (("guess", 0), propT);
2.7 + val pos = Position.thread_data ();
2.8 fun print_result ctxt' (k, [(s, [_, th])]) =
2.9 - Proof_Display.print_results int ctxt' (k, [(s, [th])]);
2.10 + Proof_Display.print_results int pos ctxt' (k, [(s, [th])]);
2.11 val before_qed =
2.12 Method.primitive_text (fn ctxt =>
2.13 Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
3.1 --- a/src/Pure/Isar/proof.ML Fri May 09 08:13:37 2014 +0200
3.2 +++ b/src/Pure/Isar/proof.ML Fri May 09 22:56:06 2014 +0200
3.3 @@ -1045,7 +1045,7 @@
3.4 local
3.5
3.6 fun gen_have prep_att prepp before_qed after_qed stmt int =
3.7 - local_goal (Proof_Display.print_results int)
3.8 + local_goal (Proof_Display.print_results int (Position.thread_data ()))
3.9 prep_att prepp "have" before_qed after_qed stmt;
3.10
3.11 fun gen_show prep_att prepp before_qed after_qed stmt int state =
3.12 @@ -1057,13 +1057,17 @@
3.13 (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
3.14 |> cat_lines;
3.15
3.16 + val pos = Position.thread_data ();
3.17 fun print_results ctxt res =
3.18 if ! testing then ()
3.19 - else Proof_Display.print_results int ctxt res;
3.20 + else Proof_Display.print_results int pos ctxt res;
3.21 fun print_rule ctxt th =
3.22 if ! testing then rule := SOME th
3.23 else if int then
3.24 - writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
3.25 + Proof_Display.string_of_rule ctxt "Successful" th
3.26 + |> Markup.markup Markup.text_fold
3.27 + |> Markup.markup Markup.state
3.28 + |> writeln
3.29 else ();
3.30 val test_proof =
3.31 local_skip_proof true
4.1 --- a/src/Pure/Isar/proof_display.ML Fri May 09 08:13:37 2014 +0200
4.2 +++ b/src/Pure/Isar/proof_display.ML Fri May 09 22:56:06 2014 +0200
4.3 @@ -22,8 +22,10 @@
4.4 val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
4.5 val method_error: string -> Position.T ->
4.6 {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
4.7 - val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
4.8 - val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
4.9 + val print_results: bool -> Position.T -> Proof.context ->
4.10 + ((string * string) * (string * thm list) list) -> unit
4.11 + val print_consts: bool -> Position.T -> Proof.context ->
4.12 + (string * typ -> bool) -> (string * typ) list -> unit
4.13 end
4.14
4.15 structure Proof_Display: PROOF_DISPLAY =
4.16 @@ -127,11 +129,13 @@
4.17
4.18 (* results *)
4.19
4.20 +fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
4.21 +
4.22 local
4.23
4.24 -fun pretty_fact_name (kind, "") = Pretty.keyword1 kind
4.25 - | pretty_fact_name (kind, name) =
4.26 - Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
4.27 +fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
4.28 + | pretty_fact_name pos (kind, name) =
4.29 + Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1,
4.30 Pretty.str (Long_Name.base_name name), Pretty.str ":"];
4.31
4.32 fun pretty_facts ctxt =
4.33 @@ -140,17 +144,18 @@
4.34
4.35 in
4.36
4.37 -fun print_results do_print ctxt ((kind, name), facts) =
4.38 +fun print_results do_print pos ctxt ((kind, name), facts) =
4.39 if not do_print orelse kind = "" then ()
4.40 else if name = "" then
4.41 (Pretty.writeln o Pretty.mark Markup.state)
4.42 - (Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
4.43 + (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
4.44 + pretty_facts ctxt facts))
4.45 else
4.46 (Pretty.writeln o Pretty.mark Markup.state)
4.47 (case facts of
4.48 - [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
4.49 + [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
4.50 Proof_Context.pretty_fact ctxt fact])
4.51 - | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
4.52 + | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
4.53 Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
4.54
4.55 end;
4.56 @@ -164,18 +169,19 @@
4.57 Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
4.58 Pretty.quote (Syntax.pretty_typ ctxt T)];
4.59
4.60 -fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
4.61 +fun pretty_vars pos ctxt kind vs =
4.62 + Pretty.block (Pretty.fbreaks (position_markup pos (Pretty.str kind) :: map (pretty_var ctxt) vs));
4.63
4.64 -fun pretty_consts ctxt pred cs =
4.65 +fun pretty_consts pos ctxt pred cs =
4.66 (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
4.67 - [] => pretty_vars ctxt "constants" cs
4.68 - | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
4.69 + [] => pretty_vars pos ctxt "constants" cs
4.70 + | ps => Pretty.chunks [pretty_vars pos ctxt "parameters" ps, pretty_vars pos ctxt "constants" cs]);
4.71
4.72 in
4.73
4.74 -fun print_consts do_print ctxt pred cs =
4.75 +fun print_consts do_print pos ctxt pred cs =
4.76 if not do_print orelse null cs then ()
4.77 - else Pretty.writeln (Pretty.mark Markup.state (pretty_consts ctxt pred cs));
4.78 + else Pretty.writeln (Pretty.mark Markup.state (pretty_consts pos ctxt pred cs));
4.79
4.80 end;
4.81
5.1 --- a/src/Pure/Isar/specification.ML Fri May 09 08:13:37 2014 +0200
5.2 +++ b/src/Pure/Isar/specification.ML Fri May 09 22:56:06 2014 +0200
5.3 @@ -223,7 +223,9 @@
5.4
5.5 val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
5.6
5.7 - val _ = Proof_Display.print_consts int lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
5.8 + val _ =
5.9 + Proof_Display.print_consts int (Position.thread_data ()) lthy4
5.10 + (member (op =) (Term.add_frees lhs' [])) [(x, T)];
5.11 in ((lhs, (def_name, th')), lthy4) end;
5.12
5.13 val definition' = gen_def check_free_spec;
5.14 @@ -256,7 +258,7 @@
5.15 |> Local_Theory.abbrev mode (var, rhs) |> snd
5.16 |> Proof_Context.restore_syntax_mode lthy;
5.17
5.18 - val _ = Proof_Display.print_consts int lthy2 (K false) [(x, T)];
5.19 + val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)];
5.20 in lthy2 end;
5.21
5.22 val abbreviation = gen_abbrev check_free_spec;
5.23 @@ -301,7 +303,7 @@
5.24 |> Attrib.partial_evaluation ctxt'
5.25 |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
5.26 val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
5.27 - val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
5.28 + val _ = Proof_Display.print_results int (Position.thread_data ()) lthy' ((kind, ""), res);
5.29 in (res, lthy') end;
5.30
5.31 in
5.32 @@ -389,6 +391,7 @@
5.33 |> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
5.34 val atts = more_atts @ map (prep_att lthy) raw_atts;
5.35
5.36 + val pos = Position.thread_data ();
5.37 fun after_qed' results goal_ctxt' =
5.38 let
5.39 val results' =
5.40 @@ -400,12 +403,12 @@
5.41 (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
5.42 val lthy'' =
5.43 if Attrib.is_empty_binding (name, atts) then
5.44 - (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
5.45 + (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy')
5.46 else
5.47 let
5.48 val ([(res_name, _)], lthy'') =
5.49 Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
5.50 - val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
5.51 + val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res);
5.52 in lthy'' end;
5.53 in after_qed results' lthy'' end;
5.54 in
6.1 --- a/src/Tools/jEdit/src/dockable.scala Fri May 09 08:13:37 2014 +0200
6.2 +++ b/src/Tools/jEdit/src/dockable.scala Fri May 09 22:56:06 2014 +0200
6.3 @@ -22,7 +22,7 @@
6.4 if (position == DockableWindowManager.FLOATING)
6.5 setPreferredSize(new Dimension(500, 250))
6.6
6.7 - def focusOnDefaultComponent { requestFocus }
6.8 + def focusOnDefaultComponent { JEdit_Lib.request_focus_view(view) }
6.9
6.10 def set_content(c: Component) { add(c, BorderLayout.CENTER) }
6.11 def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
7.1 --- a/src/Tools/jEdit/src/jedit_lib.scala Fri May 09 08:13:37 2014 +0200
7.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala Fri May 09 22:56:06 2014 +0200
7.3 @@ -326,9 +326,9 @@
7.4
7.5 /* key event handling */
7.6
7.7 - def request_focus_view
7.8 + def request_focus_view(alt_view: View = null)
7.9 {
7.10 - val view = jEdit.getActiveView()
7.11 + val view = if (alt_view != null) alt_view else jEdit.getActiveView()
7.12 if (view != null) {
7.13 val text_area = view.getTextArea
7.14 if (text_area != null) text_area.requestFocus
8.1 --- a/src/Tools/jEdit/src/output_dockable.scala Fri May 09 08:13:37 2014 +0200
8.2 +++ b/src/Tools/jEdit/src/output_dockable.scala Fri May 09 22:56:06 2014 +0200
8.3 @@ -20,9 +20,6 @@
8.4
8.5 class Output_Dockable(view: View, position: String) extends Dockable(view, position)
8.6 {
8.7 - override def focusOnDefaultComponent { view.getTextArea.requestFocus }
8.8 -
8.9 -
8.10 /* component state -- owned by Swing thread */
8.11
8.12 private var zoom_factor = 100
9.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala Fri May 09 08:13:37 2014 +0200
9.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri May 09 22:56:06 2014 +0200
9.3 @@ -136,7 +136,7 @@
9.4 case Some((old, _ :: rest)) =>
9.5 rest match {
9.6 case top :: _ => top.request_focus
9.7 - case Nil => JEdit_Lib.request_focus_view
9.8 + case Nil => JEdit_Lib.request_focus_view()
9.9 }
9.10 old.foreach(_.hide_popup)
9.11 tip.hide_popup
9.12 @@ -153,7 +153,7 @@
9.13 deactivate()
9.14 if (stack.isEmpty) false
9.15 else {
9.16 - JEdit_Lib.request_focus_view
9.17 + JEdit_Lib.request_focus_view()
9.18 stack.foreach(_.hide_popup)
9.19 stack = Nil
9.20 true