some position markup to help locating the query context, e.g. from "Info" dockable;
authorwenzelm
Thu May 08 16:15:20 2014 +0200 (2014-05-08)
changeset 56912293cd4dcfebc
parent 56911 dc3ba749d3b8
child 56913 df4cd6e1fdfa
some position markup to help locating the query context, e.g. from "Info" dockable;
src/Pure/Isar/proof.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Thu May 08 15:30:28 2014 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu May 08 16:15:20 2014 +0200
     1.3 @@ -364,8 +364,12 @@
     1.4        if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
     1.5        else if mode = Backward then Proof_Context.pretty_ctxt ctxt
     1.6        else [];
     1.7 +
     1.8 +    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
     1.9    in
    1.10 -    [Pretty.str ("proof (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1)),
    1.11 +    [Pretty.block
    1.12 +      [Pretty.mark_str (position_markup, "proof"),
    1.13 +        Pretty.str (" (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1))],
    1.14        Pretty.str ""] @
    1.15      (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
    1.16      (if verbose orelse mode = Forward then
     2.1 --- a/src/Pure/Tools/find_consts.ML	Thu May 08 15:30:28 2014 +0200
     2.2 +++ b/src/Pure/Tools/find_consts.ML	Thu May 08 16:15:20 2014 +0200
     2.3 @@ -112,9 +112,13 @@
     2.4        fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
     2.5        |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
     2.6        |> map (apsnd fst o snd);
     2.7 +
     2.8 +    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
     2.9    in
    2.10      Pretty.block
    2.11 -      (Pretty.fbreaks (Pretty.keyword1 "find_consts" :: map pretty_criterion raw_criteria)) ::
    2.12 +      (Pretty.fbreaks
    2.13 +        (Pretty.mark position_markup (Pretty.keyword1 "find_consts") ::
    2.14 +          map pretty_criterion raw_criteria)) ::
    2.15      Pretty.str "" ::
    2.16      (if null matches then [Pretty.str "found nothing"]
    2.17       else
     3.1 --- a/src/Pure/Tools/find_theorems.ML	Thu May 08 15:30:28 2014 +0200
     3.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu May 08 16:15:20 2014 +0200
     3.3 @@ -482,9 +482,12 @@
     3.4              (if returned < found
     3.5               then " (" ^ string_of_int returned ^ " displayed)"
     3.6               else ""));
     3.7 +    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
     3.8    in
     3.9      Pretty.block
    3.10 -      (Pretty.fbreaks (Pretty.keyword1 "find_theorems" :: map (pretty_criterion ctxt) criteria)) ::
    3.11 +      (Pretty.fbreaks
    3.12 +        (Pretty.mark position_markup (Pretty.keyword1 "find_theorems") ::
    3.13 +          map (pretty_criterion ctxt) criteria)) ::
    3.14      Pretty.str "" ::
    3.15      (if null theorems then [Pretty.str "found nothing"]
    3.16       else