renamed Position.str_of to Position.here;
authorwenzelm
Wed Aug 29 11:48:45 2012 +0200 (2012-08-29)
changeset 489920518bf89c777
parent 48991 0350245dec1c
child 48993 44428ea53dc1
renamed Position.str_of to Position.here;
NEWS
src/Doc/IsarImplementation/Prelim.thy
src/HOL/SPARK/Tools/fdl_lexer.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/Pure/General/antiquote.ML
src/Pure/General/binding.ML
src/Pure/General/name_space.ML
src/Pure/General/position.ML
src/Pure/General/position.scala
src/Pure/General/symbol_pos.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/token.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_lex.ML
src/Pure/ML/ml_parse.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/System/build.scala
src/Pure/System/options.scala
src/Pure/Thy/rail.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
src/Pure/consts.ML
src/Pure/context.ML
src/Pure/facts.ML
src/Pure/global_theory.ML
src/Pure/goal.ML
src/Pure/raw_simplifier.ML
src/Pure/type.ML
src/Tools/WWW_Find/unicode_symbols.ML
src/Tools/induct_tacs.ML
     1.1 --- a/NEWS	Wed Aug 29 11:31:07 2012 +0200
     1.2 +++ b/NEWS	Wed Aug 29 11:48:45 2012 +0200
     1.3 @@ -88,6 +88,13 @@
     1.4  document/IsaMakefile.  Minor INCOMPATIBILITY.
     1.5  
     1.6  
     1.7 +*** ML ***
     1.8 +
     1.9 +* Renamed Position.str_of to Position.here to emphasize that this is a
    1.10 +formal device to inline positions into message text, but not
    1.11 +necessarily printing visible text.
    1.12 +
    1.13 +
    1.14  *** System ***
    1.15  
    1.16  * The "isabelle logo" tool allows to specify EPS or PDF format; the
     2.1 --- a/src/Doc/IsarImplementation/Prelim.thy	Wed Aug 29 11:31:07 2012 +0200
     2.2 +++ b/src/Doc/IsarImplementation/Prelim.thy	Wed Aug 29 11:48:45 2012 +0200
     2.3 @@ -1226,7 +1226,7 @@
     2.4  
     2.5  ML_command {*
     2.6    writeln
     2.7 -    ("Look here" ^ Position.str_of (Binding.pos_of @{binding here}))
     2.8 +    ("Look here" ^ Position.here (Binding.pos_of @{binding here}))
     2.9  *}
    2.10  
    2.11  text {* This illustrates a key virtue of formalized bindings as
     3.1 --- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Wed Aug 29 11:31:07 2012 +0200
     3.2 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Wed Aug 29 11:48:45 2012 +0200
     3.3 @@ -56,7 +56,7 @@
     3.4  
     3.5  fun position_of (Token (_, _, pos)) = pos;
     3.6  
     3.7 -val pos_of = Position.str_of o position_of;
     3.8 +val pos_of = Position.here o position_of;
     3.9  
    3.10  fun is_eof (Token (EOF, _, _)) = true
    3.11    | is_eof _ = false;
    3.12 @@ -192,7 +192,7 @@
    3.13  fun !!! text scan =
    3.14    let
    3.15      fun get_pos [] = " (end-of-input)"
    3.16 -      | get_pos ((_, pos) :: _) = Position.str_of pos;
    3.17 +      | get_pos ((_, pos) :: _) = Position.here pos;
    3.18  
    3.19      fun err (syms, msg) = fn () =>
    3.20        text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^
     4.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Wed Aug 29 11:31:07 2012 +0200
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Wed Aug 29 11:48:45 2012 +0200
     4.3 @@ -48,7 +48,7 @@
     4.4  fun error_msg bind str =
     4.5    let
     4.6      val name = Binding.name_of bind
     4.7 -    val pos = Position.str_of (Binding.pos_of bind)
     4.8 +    val pos = Position.here (Binding.pos_of bind)
     4.9    in
    4.10      error ("Head of quotient_definition " ^
    4.11        quote str ^ " differs from declaration " ^ name ^ pos)
     5.1 --- a/src/Pure/General/antiquote.ML	Wed Aug 29 11:31:07 2012 +0200
     5.2 +++ b/src/Pure/General/antiquote.ML	Wed Aug 29 11:48:45 2012 +0200
     5.3 @@ -49,7 +49,7 @@
     5.4  (* check_nesting *)
     5.5  
     5.6  fun err_unbalanced pos =
     5.7 -  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
     5.8 +  error ("Unbalanced antiquotation block parentheses" ^ Position.here pos);
     5.9  
    5.10  fun check_nesting antiqs =
    5.11    let
    5.12 @@ -101,6 +101,6 @@
    5.13  fun read (syms, pos) =
    5.14    (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
    5.15      SOME xs => (Position.reports_text (reports_of (K []) xs); check_nesting xs; xs)
    5.16 -  | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    5.17 +  | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
    5.18  
    5.19  end;
     6.1 --- a/src/Pure/General/binding.ML	Wed Aug 29 11:31:07 2012 +0200
     6.2 +++ b/src/Pure/General/binding.ML	Wed Aug 29 11:48:45 2012 +0200
     6.3 @@ -133,7 +133,7 @@
     6.4  
     6.5  (* check *)
     6.6  
     6.7 -fun bad binding = "Bad name binding: " ^ print binding ^ Position.str_of (pos_of binding);
     6.8 +fun bad binding = "Bad name binding: " ^ print binding ^ Position.here (pos_of binding);
     6.9  
    6.10  fun check binding =
    6.11    if Symbol.is_ident (Symbol.explode (name_of binding)) then ()
     7.1 --- a/src/Pure/General/name_space.ML	Wed Aug 29 11:31:07 2012 +0200
     7.2 +++ b/src/Pure/General/name_space.ML	Wed Aug 29 11:48:45 2012 +0200
     7.3 @@ -424,7 +424,7 @@
     7.4    let val name = intern space xname in
     7.5      (case Symtab.lookup tab name of
     7.6        SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))
     7.7 -    | NONE => error (undefined (kind_of space) name ^ Position.str_of pos))
     7.8 +    | NONE => error (undefined (kind_of space) name ^ Position.here pos))
     7.9    end;
    7.10  
    7.11  fun get (space, tab) name =
     8.1 --- a/src/Pure/General/position.ML	Wed Aug 29 11:31:07 2012 +0200
     8.2 +++ b/src/Pure/General/position.ML	Wed Aug 29 11:48:45 2012 +0200
     8.3 @@ -41,7 +41,7 @@
     8.4    val reports_text: report_text list -> unit
     8.5    val reports: report list -> unit
     8.6    val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
     8.7 -  val str_of: T -> string
     8.8 +  val here: T -> string
     8.9    type range = T * T
    8.10    val no_range: range
    8.11    val set_range: range -> T
    8.12 @@ -180,9 +180,9 @@
    8.13        in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
    8.14  
    8.15  
    8.16 -(* str_of *)
    8.17 +(* here: inlined formal markup *)
    8.18  
    8.19 -fun str_of pos =
    8.20 +fun here pos =
    8.21    let
    8.22      val props = properties_of pos;
    8.23      val s =
     9.1 --- a/src/Pure/General/position.scala	Wed Aug 29 11:31:07 2012 +0200
     9.2 +++ b/src/Pure/General/position.scala	Wed Aug 29 11:48:45 2012 +0200
     9.3 @@ -71,7 +71,9 @@
     9.4        yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
     9.5  
     9.6  
     9.7 -  def str_of(pos: T): String =
     9.8 +  /* here: inlined formal markup */
     9.9 +
    9.10 +  def here(pos: T): String =
    9.11      (Line.unapply(pos), File.unapply(pos)) match {
    9.12        case (Some(i), None) => " (line " + i.toString + ")"
    9.13        case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
    10.1 --- a/src/Pure/General/symbol_pos.ML	Wed Aug 29 11:31:07 2012 +0200
    10.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Aug 29 11:48:45 2012 +0200
    10.3 @@ -67,7 +67,7 @@
    10.4  fun !!! text scan =
    10.5    let
    10.6      fun get_pos [] = " (end-of-input)"
    10.7 -      | get_pos ((_, pos) :: _) = Position.str_of pos;
    10.8 +      | get_pos ((_, pos) :: _) = Position.here pos;
    10.9  
   10.10      fun err (syms, msg) = fn () =>
   10.11        text () ^ get_pos syms ^
    11.1 --- a/src/Pure/Isar/args.ML	Wed Aug 29 11:31:07 2012 +0200
    11.2 +++ b/src/Pure/Isar/args.ML	Wed Aug 29 11:48:45 2012 +0200
    11.3 @@ -274,7 +274,7 @@
    11.4    (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of
    11.5      (SOME x, (st', [])) => (x, st')
    11.6    | (_, (_, args')) =>
    11.7 -      error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n  " ^
    11.8 +      error (kind ^ " " ^ quote s ^ Position.here pos ^ ": bad arguments\n  " ^
    11.9          space_implode " " (map Token.unparse args')));
   11.10  
   11.11  fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
    12.1 --- a/src/Pure/Isar/attrib.ML	Wed Aug 29 11:31:07 2012 +0200
    12.2 +++ b/src/Pure/Isar/attrib.ML	Wed Aug 29 11:48:45 2012 +0200
    12.3 @@ -129,7 +129,7 @@
    12.4      fun attr src =
    12.5        let val ((name, _), pos) = Args.dest_src src in
    12.6          (case Symtab.lookup tab name of
    12.7 -          NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
    12.8 +          NONE => error ("Unknown attribute: " ^ quote name ^ Position.here pos)
    12.9          | SOME (att, _) =>
   12.10              (Context_Position.report_generic context pos (Name_Space.markup space name); att src))
   12.11        end;
   12.12 @@ -254,7 +254,7 @@
   12.13  
   12.14  fun err msg src =
   12.15    let val ((name, _), pos) = Args.dest_src src
   12.16 -  in error (msg ^ " " ^ quote name ^ Position.str_of pos) end;
   12.17 +  in error (msg ^ " " ^ quote name ^ Position.here pos) end;
   12.18  
   12.19  fun eval src ((th, dyn), (decls, context)) =
   12.20    (case (apply_att src (context, th), dyn) of
    13.1 --- a/src/Pure/Isar/method.ML	Wed Aug 29 11:31:07 2012 +0200
    13.2 +++ b/src/Pure/Isar/method.ML	Wed Aug 29 11:48:45 2012 +0200
    13.3 @@ -340,7 +340,7 @@
    13.4      fun meth src =
    13.5        let val ((name, _), pos) = Args.dest_src src in
    13.6          (case Symtab.lookup tab name of
    13.7 -          NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
    13.8 +          NONE => error ("Unknown proof method: " ^ quote name ^ Position.here pos)
    13.9          | SOME (mth, _) => (Position.report pos (Name_Space.markup space name); mth src))
   13.10        end;
   13.11    in meth end;
    14.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Aug 29 11:31:07 2012 +0200
    14.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Aug 29 11:48:45 2012 +0200
    14.3 @@ -142,11 +142,11 @@
    14.4          SOME spec =>
    14.5            if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
    14.6            else error ("Inconsistent outer syntax keyword declaration " ^
    14.7 -            quote name ^ Position.str_of pos)
    14.8 +            quote name ^ Position.here pos)
    14.9        | NONE =>
   14.10            if Context.theory_name thy = Context.PureN
   14.11            then Keyword.define (name, SOME kind)
   14.12 -          else error ("Undeclared outer syntax command " ^ quote name ^ Position.str_of pos));
   14.13 +          else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
   14.14      val _ = Position.report pos (command_markup true (name, cmd));
   14.15    in
   14.16      Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
    15.1 --- a/src/Pure/Isar/proof_context.ML	Wed Aug 29 11:31:07 2012 +0200
    15.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Aug 29 11:48:45 2012 +0200
    15.3 @@ -361,7 +361,7 @@
    15.4      val tsig = tsig_of ctxt;
    15.5      val (syms, pos) = Syntax.read_token text;
    15.6      val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
    15.7 -      handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
    15.8 +      handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
    15.9      val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
   15.10    in c end;
   15.11  
   15.12 @@ -425,7 +425,7 @@
   15.13  
   15.14  fun prep_const_proper ctxt strict (c, pos) =
   15.15    let
   15.16 -    fun err msg = error (msg ^ Position.str_of pos);
   15.17 +    fun err msg = error (msg ^ Position.here pos);
   15.18      val consts = consts_of ctxt;
   15.19      val t as Const (d, _) =
   15.20        (case Variable.lookup_const ctxt c of
   15.21 @@ -452,7 +452,7 @@
   15.22        let
   15.23          val d = intern_type ctxt c;
   15.24          val decl = Type.the_decl tsig (d, pos);
   15.25 -        fun err () = error ("Bad type name: " ^ quote d ^ Position.str_of pos);
   15.26 +        fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos);
   15.27          val args =
   15.28            (case decl of
   15.29              Type.LogicalType n => n
   15.30 @@ -844,7 +844,7 @@
   15.31          val prop =
   15.32            Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
   15.33            |> singleton (Variable.polymorphic ctxt);
   15.34 -        fun err msg = error (msg ^ Position.str_of pos ^ ":\n" ^ Syntax.string_of_term ctxt prop);
   15.35 +        fun err msg = error (msg ^ Position.here pos ^ ":\n" ^ Syntax.string_of_term ctxt prop);
   15.36  
   15.37          val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
   15.38          fun prove_fact th =
    16.1 --- a/src/Pure/Isar/runtime.ML	Wed Aug 29 11:31:07 2012 +0200
    16.2 +++ b/src/Pure/Isar/runtime.ML	Wed Aug 29 11:48:45 2012 +0200
    16.3 @@ -48,7 +48,7 @@
    16.4  fun exn_messages exn_position e =
    16.5    let
    16.6      fun raised exn name msgs =
    16.7 -      let val pos = Position.str_of (exn_position exn) in
    16.8 +      let val pos = Position.here (exn_position exn) in
    16.9          (case msgs of
   16.10            [] => "exception " ^ name ^ " raised" ^ pos
   16.11          | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
    17.1 --- a/src/Pure/Isar/specification.ML	Wed Aug 29 11:31:07 2012 +0200
    17.2 +++ b/src/Pure/Isar/specification.ML	Wed Aug 29 11:48:45 2012 +0200
    17.3 @@ -210,7 +210,7 @@
    17.4              val y = Variable.check_name b;
    17.5              val _ = x = y orelse
    17.6                error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
    17.7 -                Position.str_of (Binding.pos_of b));
    17.8 +                Position.here (Binding.pos_of b));
    17.9            in (b, mx) end);
   17.10      val name = Thm.def_binding_optional b raw_name;
   17.11      val ((lhs, (_, raw_th)), lthy2) = lthy
   17.12 @@ -248,7 +248,7 @@
   17.13              val y = Variable.check_name b;
   17.14              val _ = x = y orelse
   17.15                error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
   17.16 -                Position.str_of (Binding.pos_of b));
   17.17 +                Position.here (Binding.pos_of b));
   17.18            in (b, mx) end);
   17.19      val lthy' = lthy
   17.20        |> Proof_Context.set_syntax_mode mode    (* FIXME ?!? *)
    18.1 --- a/src/Pure/Isar/token.ML	Wed Aug 29 11:31:07 2012 +0200
    18.2 +++ b/src/Pure/Isar/token.ML	Wed Aug 29 11:48:45 2012 +0200
    18.3 @@ -130,7 +130,7 @@
    18.4  fun position_of (Token ((_, (pos, _)), _, _)) = pos;
    18.5  fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
    18.6  
    18.7 -val pos_of = Position.str_of o position_of;
    18.8 +val pos_of = Position.here o position_of;
    18.9  
   18.10  
   18.11  (* control tokens *)
   18.12 @@ -244,7 +244,7 @@
   18.13  
   18.14  fun put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
   18.15    | put_files _ tok =
   18.16 -      raise Fail ("Cannot put inlined files here" ^ Position.str_of (position_of tok));
   18.17 +      raise Fail ("Cannot put inlined files here" ^ Position.here (position_of tok));
   18.18  
   18.19  
   18.20  (* access values *)
   18.21 @@ -402,7 +402,7 @@
   18.22  
   18.23  fun read_antiq lex scan (syms, pos) =
   18.24    let
   18.25 -    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
   18.26 +    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
   18.27        "@{" ^ Symbol_Pos.content syms ^ "}");
   18.28  
   18.29      val res =
    19.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 29 11:31:07 2012 +0200
    19.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 29 11:48:45 2012 +0200
    19.3 @@ -189,8 +189,8 @@
    19.4    | _ => raise UNDEF);
    19.5  
    19.6  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
    19.7 -  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.str_of pos)
    19.8 -  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);
    19.9 +  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
   19.10 +  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
   19.11  
   19.12  
   19.13  (* print state *)
   19.14 @@ -359,7 +359,7 @@
   19.15  fun print_of (Transition {print, ...}) = print;
   19.16  fun name_of (Transition {name, ...}) = name;
   19.17  fun pos_of (Transition {pos, ...}) = pos;
   19.18 -fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr);
   19.19 +fun str_of tr = quote (name_of tr) ^ Position.here (pos_of tr);
   19.20  
   19.21  fun command_msg msg tr = msg ^ "command " ^ str_of tr;
   19.22  fun at_command tr = command_msg "At " tr;
    20.1 --- a/src/Pure/ML/ml_antiquote.ML	Wed Aug 29 11:31:07 2012 +0200
    20.2 +++ b/src/Pure/ML/ml_antiquote.ML	Wed Aug 29 11:48:45 2012 +0200
    20.3 @@ -139,7 +139,7 @@
    20.4        val res =
    20.5          (case try check (c, decl) of
    20.6            SOME res => res
    20.7 -        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos));
    20.8 +        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
    20.9      in ML_Syntax.print_string res end);
   20.10  
   20.11  val _ = Context.>> (Context.map_theory
   20.12 @@ -160,7 +160,7 @@
   20.13      let
   20.14        val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
   20.15        val res = check (Proof_Context.consts_of ctxt, c)
   20.16 -        handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
   20.17 +        handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   20.18      in ML_Syntax.print_string res end);
   20.19  
   20.20  val _ = Context.>> (Context.map_theory
   20.21 @@ -175,7 +175,7 @@
   20.22      (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   20.23        if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   20.24        then ML_Syntax.print_string c
   20.25 -      else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))) #>
   20.26 +      else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
   20.27  
   20.28    inline (Binding.name "const")
   20.29      (Args.context -- Scan.lift Args.name_source -- Scan.optional
   20.30 @@ -197,14 +197,14 @@
   20.31  fun with_keyword f =
   20.32    Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
   20.33      (f ((name, Thy_Header.the_keyword thy name), pos)
   20.34 -      handle ERROR msg => error (msg ^ Position.str_of pos)));
   20.35 +      handle ERROR msg => error (msg ^ Position.here pos)));
   20.36  
   20.37  val _ = Context.>> (Context.map_theory
   20.38   (value (Binding.name "keyword")
   20.39      (with_keyword
   20.40        (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
   20.41          | ((name, SOME _), pos) =>
   20.42 -            error ("Expected minor keyword " ^ quote name ^ Position.str_of pos))) #>
   20.43 +            error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
   20.44    value (Binding.name "command_spec")
   20.45      (with_keyword
   20.46        (fn ((name, SOME kind), pos) =>
   20.47 @@ -217,7 +217,7 @@
   20.48                    (ML_Syntax.print_list ML_Syntax.print_string)))
   20.49                ML_Syntax.print_position) ((name, kind), pos))
   20.50          | ((name, NONE), pos) =>
   20.51 -            error ("Expected command keyword " ^ quote name ^ Position.str_of pos)))));
   20.52 +            error ("Expected command keyword " ^ quote name ^ Position.here pos)))));
   20.53  
   20.54  end;
   20.55  
    21.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Aug 29 11:31:07 2012 +0200
    21.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Aug 29 11:48:45 2012 +0200
    21.3 @@ -114,7 +114,7 @@
    21.4          val pos = position_of loc;
    21.5          val txt =
    21.6            (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
    21.7 -            ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
    21.8 +            ((if hard then "Error" else "Warning") ^ Position.here pos ^ ":\n") ^
    21.9            Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
   21.10            Position.reported_text pos Isabelle_Markup.report "";
   21.11        in if hard then err txt else warn txt end;
    22.1 --- a/src/Pure/ML/ml_context.ML	Wed Aug 29 11:31:07 2012 +0200
    22.2 +++ b/src/Pure/ML/ml_context.ML	Wed Aug 29 11:48:45 2012 +0200
    22.3 @@ -150,7 +150,7 @@
    22.4          let
    22.5            val ctxt =
    22.6              (case opt_ctxt of
    22.7 -              NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.str_of pos)
    22.8 +              NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos)
    22.9              | SOME ctxt => Context.proof_of ctxt);
   22.10  
   22.11            val lex = #1 (Keyword.get_lexicons ());
    23.1 --- a/src/Pure/ML/ml_env.ML	Wed Aug 29 11:31:07 2012 +0200
    23.2 +++ b/src/Pure/ML/ml_env.ML	Wed Aug 29 11:48:45 2012 +0200
    23.3 @@ -85,7 +85,7 @@
    23.4  val local_context: use_context =
    23.5   {tune_source = ML_Parse.fix_ints,
    23.6    name_space = name_space,
    23.7 -  str_of_pos = Position.str_of oo Position.line_file,
    23.8 +  str_of_pos = Position.here oo Position.line_file,
    23.9    print = writeln,
   23.10    error = error};
   23.11  
    24.1 --- a/src/Pure/ML/ml_lex.ML	Wed Aug 29 11:31:07 2012 +0200
    24.2 +++ b/src/Pure/ML/ml_lex.ML	Wed Aug 29 11:48:45 2012 +0200
    24.3 @@ -82,7 +82,7 @@
    24.4      Token (_, (Keyword, ":>")) =>
    24.5        warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
    24.6          \prefer non-opaque matching (:) possibly with abstype" ^
    24.7 -        Position.str_of (pos_of tok))
    24.8 +        Position.here (pos_of tok))
    24.9    | _ => ());
   24.10  
   24.11  fun check_content_of tok =
   24.12 @@ -307,7 +307,7 @@
   24.13          |> tap Antiquote.check_nesting
   24.14          |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
   24.15        handle ERROR msg =>
   24.16 -        cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
   24.17 +        cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos);
   24.18    in input @ termination end;
   24.19  
   24.20  end;
    25.1 --- a/src/Pure/ML/ml_parse.ML	Wed Aug 29 11:31:07 2012 +0200
    25.2 +++ b/src/Pure/ML/ml_parse.ML	Wed Aug 29 11:48:45 2012 +0200
    25.3 @@ -18,7 +18,7 @@
    25.4  fun !!! scan =
    25.5    let
    25.6      fun get_pos [] = " (end-of-input)"
    25.7 -      | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok);
    25.8 +      | get_pos (tok :: _) = Position.here (ML_Lex.pos_of tok);
    25.9  
   25.10      fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks)
   25.11        | err (toks, SOME msg) = (fn () => "SML syntax error" ^ get_pos toks ^ ": " ^ msg ());
   25.12 @@ -67,7 +67,7 @@
   25.13  val global_context: use_context =
   25.14   {tune_source = fix_ints,
   25.15    name_space = ML_Name_Space.global,
   25.16 -  str_of_pos = Position.str_of oo Position.line_file,
   25.17 +  str_of_pos = Position.here oo Position.line_file,
   25.18    print = writeln,
   25.19    error = error};
   25.20  
    26.1 --- a/src/Pure/Syntax/lexicon.ML	Wed Aug 29 11:31:07 2012 +0200
    26.2 +++ b/src/Pure/Syntax/lexicon.ML	Wed Aug 29 11:48:45 2012 +0200
    26.3 @@ -298,7 +298,7 @@
    26.4          (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
    26.5        (toks, []) => toks
    26.6      | (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^
    26.7 -        Position.str_of (#1 (Symbol_Pos.range ss))))
    26.8 +        Position.here (#1 (Symbol_Pos.range ss))))
    26.9    end;
   26.10  
   26.11  
    27.1 --- a/src/Pure/Syntax/parser.ML	Wed Aug 29 11:31:07 2012 +0200
    27.2 +++ b/src/Pure/Syntax/parser.ML	Wed Aug 29 11:48:45 2012 +0200
    27.3 @@ -702,7 +702,7 @@
    27.4      [] =>
    27.5        let
    27.6          val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata;
    27.7 -        val pos = Position.str_of (Lexicon.pos_of_token prev_token);
    27.8 +        val pos = Position.here (Lexicon.pos_of_token prev_token);
    27.9        in
   27.10          if null toks then error ("Inner syntax error: unexpected end of input" ^ pos)
   27.11          else error (Pretty.string_of (Pretty.block
    28.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Aug 29 11:31:07 2012 +0200
    28.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Aug 29 11:48:45 2012 +0200
    28.3 @@ -142,7 +142,7 @@
    28.4            let
    28.5              val pos = Lexicon.pos_of_token tok;
    28.6              val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok)
    28.7 -              handle ERROR msg => error (msg ^ Position.str_of pos);
    28.8 +              handle ERROR msg => error (msg ^ Position.here pos);
    28.9              val _ = report pos (markup_class ctxt) c;
   28.10            in [Ast.Constant (Lexicon.mark_class c)] end
   28.11        | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
   28.12 @@ -150,7 +150,7 @@
   28.13              val pos = Lexicon.pos_of_token tok;
   28.14              val Type (c, _) =
   28.15                Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok)
   28.16 -                handle ERROR msg => error (msg ^ Position.str_of pos);
   28.17 +                handle ERROR msg => error (msg ^ Position.here pos);
   28.18              val _ = report pos (markup_type ctxt) c;
   28.19            in [Ast.Constant (Lexicon.mark_type c)] end
   28.20        | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
   28.21 @@ -268,7 +268,7 @@
   28.22    | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
   28.23    | _ =>
   28.24        if null ambig_msgs then
   28.25 -        error ("Parse error: ambiguous syntax" ^ Position.str_of pos)
   28.26 +        error ("Parse error: ambiguous syntax" ^ Position.here pos)
   28.27        else error (cat_lines ambig_msgs));
   28.28  
   28.29  
   28.30 @@ -294,7 +294,7 @@
   28.31        if len <= 1 then []
   28.32        else
   28.33          [cat_lines
   28.34 -          (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^
   28.35 +          (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
   28.36              "\nproduces " ^ string_of_int len ^ " parse trees" ^
   28.37              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   28.38              map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))];
   28.39 @@ -379,7 +379,7 @@
   28.40                Context_Position.if_visible ctxt warning
   28.41                  (cat_lines (ambig_msgs @
   28.42                    ["Fortunately, only one parse tree is type correct" ^
   28.43 -                  Position.str_of (Position.reset_range pos) ^
   28.44 +                  Position.here (Position.reset_range pos) ^
   28.45                    ",\nbut you may still want to disambiguate your grammar or your input."]))
   28.46               else (); report_result ctxt pos [] results')
   28.47            else
   28.48 @@ -687,7 +687,7 @@
   28.49    | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =
   28.50        (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
   28.51          handle ERROR msg =>
   28.52 -          error (msg ^ Position.str_of (the_default Position.none (Term_Position.decode pos))))
   28.53 +          error (msg ^ Position.here (the_default Position.none (Term_Position.decode pos))))
   28.54    | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
   28.55  
   28.56  
    29.1 --- a/src/Pure/System/build.scala	Wed Aug 29 11:31:07 2012 +0200
    29.2 +++ b/src/Pure/System/build.scala	Wed Aug 29 11:48:45 2012 +0200
    29.3 @@ -73,7 +73,7 @@
    29.4      catch {
    29.5        case ERROR(msg) =>
    29.6          error(msg + "\nThe error(s) above occurred in session entry " +
    29.7 -          quote(entry.name) + Position.str_of(entry.pos))
    29.8 +          quote(entry.name) + Position.here(entry.pos))
    29.9      }
   29.10  
   29.11  
   29.12 @@ -87,7 +87,7 @@
   29.13          (Graph.string[Session_Info] /: infos) {
   29.14            case (graph, (name, info)) =>
   29.15              if (graph.defined(name))
   29.16 -              error("Duplicate session " + quote(name) + Position.str_of(info.pos))
   29.17 +              error("Duplicate session " + quote(name) + Position.here(info.pos))
   29.18              else graph.new_node(name, info)
   29.19          }
   29.20        val graph2 =
   29.21 @@ -98,7 +98,7 @@
   29.22                case Some(parent) =>
   29.23                  if (!graph.defined(parent))
   29.24                    error("Bad parent session " + quote(parent) + " for " +
   29.25 -                    quote(name) + Position.str_of(info.pos))
   29.26 +                    quote(name) + Position.here(info.pos))
   29.27  
   29.28                  try { graph.add_edge_acyclic(parent, name) }
   29.29                  catch {
   29.30 @@ -106,7 +106,7 @@
   29.31                      error(cat_lines(exn.cycles.map(cycle =>
   29.32                        "Cyclic session dependency of " +
   29.33                          cycle.map(c => quote(c.toString)).mkString(" via "))) +
   29.34 -                          Position.str_of(info.pos))
   29.35 +                          Position.here(info.pos))
   29.36                  }
   29.37              }
   29.38          }
   29.39 @@ -374,7 +374,7 @@
   29.40              catch {
   29.41                case ERROR(msg) =>
   29.42                  error(msg + "\nThe error(s) above occurred in session " +
   29.43 -                  quote(name) + Position.str_of(info.pos))
   29.44 +                  quote(name) + Position.here(info.pos))
   29.45              }
   29.46            val errors = parent_errors ::: thy_deps.deps.map(d => d._2.errors).flatten
   29.47  
    30.1 --- a/src/Pure/System/options.scala	Wed Aug 29 11:31:07 2012 +0200
    30.2 +++ b/src/Pure/System/options.scala	Wed Aug 29 11:48:45 2012 +0200
    30.3 @@ -77,7 +77,7 @@
    30.4            case bad => error(bad.toString)
    30.5          }
    30.6        try { (options /: ops) { case (opts, op) => op(opts) } }
    30.7 -      catch { case ERROR(msg) => error(msg + Position.str_of(file.position)) }
    30.8 +      catch { case ERROR(msg) => error(msg + Position.here(file.position)) }
    30.9      }
   30.10    }
   30.11  
    31.1 --- a/src/Pure/Thy/rail.ML	Wed Aug 29 11:31:07 2012 +0200
    31.2 +++ b/src/Pure/Thy/rail.ML	Wed Aug 29 11:48:45 2012 +0200
    31.3 @@ -35,7 +35,7 @@
    31.4  
    31.5  fun print (Token ((pos, _), (k, x))) =
    31.6    (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
    31.7 -  Position.str_of pos;
    31.8 +  Position.here pos;
    31.9  
   31.10  fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
   31.11  
   31.12 @@ -92,7 +92,7 @@
   31.13      val prefix = "Rail syntax error";
   31.14  
   31.15      fun get_pos [] = " (end-of-input)"
   31.16 -      | get_pos (tok :: _) = Position.str_of (pos_of tok);
   31.17 +      | get_pos (tok :: _) = Position.here (pos_of tok);
   31.18  
   31.19      fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
   31.20        | err (toks, SOME msg) =
    32.1 --- a/src/Pure/Thy/thy_header.ML	Wed Aug 29 11:31:07 2012 +0200
    32.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Aug 29 11:48:45 2012 +0200
    32.3 @@ -140,7 +140,7 @@
    32.4    in
    32.5      (case res of
    32.6        SOME (h, _) => h
    32.7 -    | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
    32.8 +    | NONE => error ("Unexpected end of input" ^ Position.here pos))
    32.9    end;
   32.10  
   32.11  fun read pos str = read_source pos (token_source pos str);
    33.1 --- a/src/Pure/Thy/thy_info.ML	Wed Aug 29 11:31:07 2012 +0200
    33.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Aug 29 11:48:45 2012 +0200
    33.3 @@ -274,7 +274,7 @@
    33.4            val (current, deps, theory_pos, imports, uses, keywords) = check_deps dir' name
    33.5              handle ERROR msg => cat_error msg
    33.6                (loader_msg "the error(s) above occurred while examining theory" [name] ^
    33.7 -                Position.str_of require_pos ^ required_by "\n" initiators);
    33.8 +                Position.here require_pos ^ required_by "\n" initiators);
    33.9  
   33.10            val parents = map (base_name o #1) imports;
   33.11            val (parents_current, tasks') =
    34.1 --- a/src/Pure/Thy/thy_load.ML	Wed Aug 29 11:31:07 2012 +0200
    34.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Aug 29 11:48:45 2012 +0200
    34.3 @@ -109,7 +109,7 @@
    34.4      Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks) =>
    34.5        if Keyword.is_theory_load cmd then
    34.6          (case find_file toks of
    34.7 -          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.str_of pos)
    34.8 +          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
    34.9          | SOME (i, path) =>
   34.10              let
   34.11                val toks' = toks |> map_index (fn (j, tok) =>
   34.12 @@ -135,7 +135,7 @@
   34.13      val {name = (name, pos), imports, uses, keywords} =
   34.14        Thy_Header.read (Path.position master_file) text;
   34.15      val _ = thy_name <> name andalso
   34.16 -      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.str_of pos);
   34.17 +      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
   34.18    in
   34.19     {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
   34.20      imports = imports, uses = uses, keywords = keywords}
    35.1 --- a/src/Pure/Thy/thy_output.ML	Wed Aug 29 11:31:07 2012 +0200
    35.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Aug 29 11:48:45 2012 +0200
    35.3 @@ -110,7 +110,7 @@
    35.4    in
    35.5      f src state ctxt handle ERROR msg =>
    35.6        cat_error msg ("The error(s) above occurred in document antiquotation: " ^
    35.7 -        quote name ^ Position.str_of pos)
    35.8 +        quote name ^ Position.here pos)
    35.9    end;
   35.10  
   35.11  fun option ((xname, pos), s) ctxt =
   35.12 @@ -198,7 +198,7 @@
   35.13      val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
   35.14    in
   35.15      if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
   35.16 -      error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
   35.17 +      error ("Unknown context -- cannot expand document antiquotations" ^ Position.here pos)
   35.18      else implode (map expand ants)
   35.19    end;
   35.20  
   35.21 @@ -309,7 +309,7 @@
   35.22        else
   35.23          (case drop (~ nesting - 1) tags of
   35.24            tgs :: tgss => (tgs, tgss)
   35.25 -        | [] => err_bad_nesting (Position.str_of cmd_pos));
   35.26 +        | [] => err_bad_nesting (Position.here cmd_pos));
   35.27  
   35.28      val buffer' =
   35.29        buffer
   35.30 @@ -535,7 +535,7 @@
   35.31  fun pretty_theory ctxt (name, pos) =
   35.32    (case find_first (fn thy => Context.theory_name thy = name)
   35.33        (Theory.nodes_of (Proof_Context.theory_of ctxt)) of
   35.34 -    NONE => error ("No ancestor theory " ^ quote name ^ Position.str_of pos)
   35.35 +    NONE => error ("No ancestor theory " ^ quote name ^ Position.here pos)
   35.36    | SOME thy => (Position.report pos (Theory.get_markup thy); Pretty.str name));
   35.37  
   35.38  
    36.1 --- a/src/Pure/consts.ML	Wed Aug 29 11:31:07 2012 +0200
    36.2 +++ b/src/Pure/consts.ML	Wed Aug 29 11:48:45 2012 +0200
    36.3 @@ -146,7 +146,7 @@
    36.4  fun read_const consts (raw_c, pos) =
    36.5    let
    36.6      val c = intern consts raw_c;
    36.7 -    val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
    36.8 +    val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
    36.9    in Const (c, T) end;
   36.10  
   36.11  
    37.1 --- a/src/Pure/context.ML	Wed Aug 29 11:31:07 2012 +0200
    37.2 +++ b/src/Pure/context.ML	Wed Aug 29 11:48:45 2012 +0200
    37.3 @@ -135,7 +135,7 @@
    37.4    (case Datatab.lookup (Synchronized.value kinds) k of
    37.5      SOME kind =>
    37.6        if ! timing andalso name <> "" then
    37.7 -        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.str_of (#pos kind))
    37.8 +        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
    37.9            (fn () => f kind x)
   37.10        else f kind x
   37.11    | NONE => raise Fail "Invalid theory data identifier");
    38.1 --- a/src/Pure/facts.ML	Wed Aug 29 11:31:07 2012 +0200
    38.2 +++ b/src/Pure/facts.ML	Wed Aug 29 11:48:45 2012 +0200
    38.3 @@ -100,7 +100,7 @@
    38.4          val n = length ths;
    38.5          fun err msg =
    38.6            error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
    38.7 -            Position.str_of pos);
    38.8 +            Position.here pos);
    38.9          fun sel i =
   38.10            if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
   38.11            else nth ths (i - 1);
    39.1 --- a/src/Pure/global_theory.ML	Wed Aug 29 11:31:07 2012 +0200
    39.2 +++ b/src/Pure/global_theory.ML	Wed Aug 29 11:48:45 2012 +0200
    39.3 @@ -103,7 +103,7 @@
    39.4      val _ = Theory.check_thy thy;
    39.5    in
    39.6      (case res of
    39.7 -      NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
    39.8 +      NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)
    39.9      | SOME (static, ths) =>
   39.10          (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
   39.11           if static then ()
    40.1 --- a/src/Pure/goal.ML	Wed Aug 29 11:31:07 2012 +0200
    40.2 +++ b/src/Pure/goal.ML	Wed Aug 29 11:48:45 2012 +0200
    40.3 @@ -208,7 +208,7 @@
    40.4      fun err msg = cat_error msg
    40.5        ("The error(s) above occurred for the goal statement:\n" ^
    40.6          string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
    40.7 -        (case Position.str_of pos of "" => "" | s => "\n" ^ s));
    40.8 +        (case Position.here pos of "" => "" | s => "\n" ^ s));
    40.9  
   40.10      fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
   40.11        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    41.1 --- a/src/Pure/raw_simplifier.ML	Wed Aug 29 11:31:07 2012 +0200
    41.2 +++ b/src/Pure/raw_simplifier.ML	Wed Aug 29 11:48:45 2012 +0200
    41.3 @@ -1057,7 +1057,7 @@
    41.4                   val _ =
    41.5                     if b <> b' then
    41.6                       warning ("Simplifier: renamed bound variable " ^
    41.7 -                       quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ()))
    41.8 +                       quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ()))
    41.9                     else ();
   41.10                   val ss' = add_bound ((b', T), a) ss;
   41.11                   val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
    42.1 --- a/src/Pure/type.ML	Wed Aug 29 11:31:07 2012 +0200
    42.2 +++ b/src/Pure/type.ML	Wed Aug 29 11:48:45 2012 +0200
    42.3 @@ -258,7 +258,7 @@
    42.4  
    42.5  fun the_decl tsig (c, pos) =
    42.6    (case lookup_type tsig c of
    42.7 -    NONE => error (undecl_type c ^ Position.str_of pos)
    42.8 +    NONE => error (undecl_type c ^ Position.here pos)
    42.9    | SOME decl => decl);
   42.10  
   42.11  
    43.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Wed Aug 29 11:31:07 2012 +0200
    43.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Wed Aug 29 11:48:45 2012 +0200
    43.3 @@ -109,7 +109,7 @@
    43.4        (toks, []) => toks
    43.5      | (_, ss) =>
    43.6          error ("Lexical error at: " ^ Symbol_Pos.content ss ^
    43.7 -          Position.str_of (#1 (Symbol_Pos.range ss))))
    43.8 +          Position.here (#1 (Symbol_Pos.range ss))))
    43.9    end;
   43.10  
   43.11  val stopper =
   43.12 @@ -152,8 +152,8 @@
   43.13          Symtab.update_new (abbr, uni) fromabbr,
   43.14          Inttab.update (uni, sym) tosym,
   43.15          Inttab.update (uni, abbr) toabbr))
   43.16 -  handle Symtab.DUP sym => error ("Duplicate at" ^ Position.str_of pos)
   43.17 -       | Inttab.DUP sym => error ("Duplicate code at" ^ Position.str_of pos);
   43.18 +  handle Symtab.DUP sym => error ("Duplicate at" ^ Position.here pos)
   43.19 +       | Inttab.DUP sym => error ("Duplicate code at" ^ Position.here pos);
   43.20  
   43.21  in
   43.22  
    44.1 --- a/src/Tools/induct_tacs.ML	Wed Aug 29 11:31:07 2012 +0200
    44.2 +++ b/src/Tools/induct_tacs.ML	Wed Aug 29 11:48:45 2012 +0200
    44.3 @@ -23,7 +23,7 @@
    44.4      val u = singleton (Variable.polymorphic ctxt) t;
    44.5      val U = Term.fastype_of u;
    44.6      val _ = Term.is_TVar U andalso
    44.7 -      error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u ^ Position.str_of pos);
    44.8 +      error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u ^ Position.here pos);
    44.9    in (u, U) end;
   44.10  
   44.11  fun gen_case_tac ctxt0 s opt_rule i st =
   44.12 @@ -75,17 +75,17 @@
   44.13          val pos = Syntax.read_token_pos name;
   44.14          val (x, _) = Term.dest_Free t handle TERM _ =>
   44.15            error ("Induction argument not a variable: " ^
   44.16 -            Syntax.string_of_term ctxt t ^ Position.str_of pos);
   44.17 +            Syntax.string_of_term ctxt t ^ Position.here pos);
   44.18          val eq_x = fn Free (y, _) => x = y | _ => false;
   44.19          val _ =
   44.20            if Term.exists_subterm eq_x concl then ()
   44.21            else
   44.22              error ("No such variable in subgoal: " ^
   44.23 -              Syntax.string_of_term ctxt t ^ Position.str_of pos);
   44.24 +              Syntax.string_of_term ctxt t ^ Position.here pos);
   44.25          val _ =
   44.26            if (exists o Term.exists_subterm) eq_x prems then
   44.27              warning ("Induction variable occurs also among premises: " ^
   44.28 -              Syntax.string_of_term ctxt t ^ Position.str_of pos)
   44.29 +              Syntax.string_of_term ctxt t ^ Position.here pos)
   44.30            else ();
   44.31        in #1 (check_type ctxt (t, pos)) end;
   44.32