# HG changeset patch # User wenzelm # Date 1346233725 -7200 # Node ID 0518bf89c7778014e33bbcc9395793b233f9373d # Parent 0350245dec1cf31bc3047903229254068e30d04e renamed Position.str_of to Position.here; diff -r 0350245dec1c -r 0518bf89c777 NEWS --- a/NEWS Wed Aug 29 11:31:07 2012 +0200 +++ b/NEWS Wed Aug 29 11:48:45 2012 +0200 @@ -88,6 +88,13 @@ document/IsaMakefile. Minor INCOMPATIBILITY. +*** ML *** + +* Renamed Position.str_of to Position.here to emphasize that this is a +formal device to inline positions into message text, but not +necessarily printing visible text. + + *** System *** * The "isabelle logo" tool allows to specify EPS or PDF format; the diff -r 0350245dec1c -r 0518bf89c777 src/Doc/IsarImplementation/Prelim.thy --- a/src/Doc/IsarImplementation/Prelim.thy Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Doc/IsarImplementation/Prelim.thy Wed Aug 29 11:48:45 2012 +0200 @@ -1226,7 +1226,7 @@ ML_command {* writeln - ("Look here" ^ Position.str_of (Binding.pos_of @{binding here})) + ("Look here" ^ Position.here (Binding.pos_of @{binding here})) *} text {* This illustrates a key virtue of formalized bindings as diff -r 0350245dec1c -r 0518bf89c777 src/HOL/SPARK/Tools/fdl_lexer.ML --- a/src/HOL/SPARK/Tools/fdl_lexer.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML Wed Aug 29 11:48:45 2012 +0200 @@ -56,7 +56,7 @@ fun position_of (Token (_, _, pos)) = pos; -val pos_of = Position.str_of o position_of; +val pos_of = Position.here o position_of; fun is_eof (Token (EOF, _, _)) = true | is_eof _ = false; @@ -192,7 +192,7 @@ fun !!! text scan = let fun get_pos [] = " (end-of-input)" - | get_pos ((_, pos) :: _) = Position.str_of pos; + | get_pos ((_, pos) :: _) = Position.here pos; fun err (syms, msg) = fn () => text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^ diff -r 0350245dec1c -r 0518bf89c777 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Wed Aug 29 11:48:45 2012 +0200 @@ -48,7 +48,7 @@ fun error_msg bind str = let val name = Binding.name_of bind - val pos = Position.str_of (Binding.pos_of bind) + val pos = Position.here (Binding.pos_of bind) in error ("Head of quotient_definition " ^ quote str ^ " differs from declaration " ^ name ^ pos) diff -r 0350245dec1c -r 0518bf89c777 src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/General/antiquote.ML Wed Aug 29 11:48:45 2012 +0200 @@ -49,7 +49,7 @@ (* check_nesting *) fun err_unbalanced pos = - error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos); + error ("Unbalanced antiquotation block parentheses" ^ Position.here pos); fun check_nesting antiqs = let @@ -101,6 +101,6 @@ fun read (syms, pos) = (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of SOME xs => (Position.reports_text (reports_of (K []) xs); check_nesting xs; xs) - | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); + | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos)); end; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/General/binding.ML Wed Aug 29 11:48:45 2012 +0200 @@ -133,7 +133,7 @@ (* check *) -fun bad binding = "Bad name binding: " ^ print binding ^ Position.str_of (pos_of binding); +fun bad binding = "Bad name binding: " ^ print binding ^ Position.here (pos_of binding); fun check binding = if Symbol.is_ident (Symbol.explode (name_of binding)) then () diff -r 0350245dec1c -r 0518bf89c777 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/General/name_space.ML Wed Aug 29 11:48:45 2012 +0200 @@ -424,7 +424,7 @@ let val name = intern space xname in (case Symtab.lookup tab name of SOME x => (Context_Position.report_generic context pos (markup space name); (name, x)) - | NONE => error (undefined (kind_of space) name ^ Position.str_of pos)) + | NONE => error (undefined (kind_of space) name ^ Position.here pos)) end; fun get (space, tab) name = diff -r 0350245dec1c -r 0518bf89c777 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/General/position.ML Wed Aug 29 11:48:45 2012 +0200 @@ -41,7 +41,7 @@ val reports_text: report_text list -> unit val reports: report list -> unit val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit - val str_of: T -> string + val here: T -> string type range = T * T val no_range: range val set_range: range -> T @@ -180,9 +180,9 @@ in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end; -(* str_of *) +(* here: inlined formal markup *) -fun str_of pos = +fun here pos = let val props = properties_of pos; val s = diff -r 0350245dec1c -r 0518bf89c777 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/General/position.scala Wed Aug 29 11:48:45 2012 +0200 @@ -71,7 +71,9 @@ yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y)) - def str_of(pos: T): String = + /* here: inlined formal markup */ + + def here(pos: T): String = (Line.unapply(pos), File.unapply(pos)) match { case (Some(i), None) => " (line " + i.toString + ")" case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")" diff -r 0350245dec1c -r 0518bf89c777 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/General/symbol_pos.ML Wed Aug 29 11:48:45 2012 +0200 @@ -67,7 +67,7 @@ fun !!! text scan = let fun get_pos [] = " (end-of-input)" - | get_pos ((_, pos) :: _) = Position.str_of pos; + | get_pos ((_, pos) :: _) = Position.here pos; fun err (syms, msg) = fn () => text () ^ get_pos syms ^ diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Isar/args.ML Wed Aug 29 11:48:45 2012 +0200 @@ -274,7 +274,7 @@ (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of (SOME x, (st', [])) => (x, st') | (_, (_, args')) => - error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n " ^ + error (kind ^ " " ^ quote s ^ Position.here pos ^ ": bad arguments\n " ^ space_implode " " (map Token.unparse args'))); fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Isar/attrib.ML Wed Aug 29 11:48:45 2012 +0200 @@ -129,7 +129,7 @@ fun attr src = let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup tab name of - NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos) + NONE => error ("Unknown attribute: " ^ quote name ^ Position.here pos) | SOME (att, _) => (Context_Position.report_generic context pos (Name_Space.markup space name); att src)) end; @@ -254,7 +254,7 @@ fun err msg src = let val ((name, _), pos) = Args.dest_src src - in error (msg ^ " " ^ quote name ^ Position.str_of pos) end; + in error (msg ^ " " ^ quote name ^ Position.here pos) end; fun eval src ((th, dyn), (decls, context)) = (case (apply_att src (context, th), dyn) of diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Isar/method.ML Wed Aug 29 11:48:45 2012 +0200 @@ -340,7 +340,7 @@ fun meth src = let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup tab name of - NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos) + NONE => error ("Unknown proof method: " ^ quote name ^ Position.here pos) | SOME (mth, _) => (Position.report pos (Name_Space.markup space name); mth src)) end; in meth end; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Wed Aug 29 11:48:45 2012 +0200 @@ -142,11 +142,11 @@ SOME spec => if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then () else error ("Inconsistent outer syntax keyword declaration " ^ - quote name ^ Position.str_of pos) + quote name ^ Position.here pos) | NONE => if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind) - else error ("Undeclared outer syntax command " ^ quote name ^ Position.str_of pos)); + else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos)); val _ = Position.report pos (command_markup true (name, cmd)); in Unsynchronized.change global_outer_syntax (map_commands (fn commands => diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Aug 29 11:48:45 2012 +0200 @@ -361,7 +361,7 @@ val tsig = tsig_of ctxt; val (syms, pos) = Syntax.read_token text; val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms)) - handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos); + handle TYPE (msg, _, _) => error (msg ^ Position.here pos); val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c); in c end; @@ -425,7 +425,7 @@ fun prep_const_proper ctxt strict (c, pos) = let - fun err msg = error (msg ^ Position.str_of pos); + fun err msg = error (msg ^ Position.here pos); val consts = consts_of ctxt; val t as Const (d, _) = (case Variable.lookup_const ctxt c of @@ -452,7 +452,7 @@ let val d = intern_type ctxt c; val decl = Type.the_decl tsig (d, pos); - fun err () = error ("Bad type name: " ^ quote d ^ Position.str_of pos); + fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos); val args = (case decl of Type.LogicalType n => n @@ -844,7 +844,7 @@ val prop = Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s |> singleton (Variable.polymorphic ctxt); - fun err msg = error (msg ^ Position.str_of pos ^ ":\n" ^ Syntax.string_of_term ctxt prop); + fun err msg = error (msg ^ Position.here pos ^ ":\n" ^ Syntax.string_of_term ctxt prop); val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1); fun prove_fact th = diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Isar/runtime.ML Wed Aug 29 11:48:45 2012 +0200 @@ -48,7 +48,7 @@ fun exn_messages exn_position e = let fun raised exn name msgs = - let val pos = Position.str_of (exn_position exn) in + let val pos = Position.here (exn_position exn) in (case msgs of [] => "exception " ^ name ^ " raised" ^ pos | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Isar/specification.ML Wed Aug 29 11:48:45 2012 +0200 @@ -210,7 +210,7 @@ val y = Variable.check_name b; val _ = x = y orelse error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ - Position.str_of (Binding.pos_of b)); + Position.here (Binding.pos_of b)); in (b, mx) end); val name = Thm.def_binding_optional b raw_name; val ((lhs, (_, raw_th)), lthy2) = lthy @@ -248,7 +248,7 @@ val y = Variable.check_name b; val _ = x = y orelse error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^ - Position.str_of (Binding.pos_of b)); + Position.here (Binding.pos_of b)); in (b, mx) end); val lthy' = lthy |> Proof_Context.set_syntax_mode mode (* FIXME ?!? *) diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Isar/token.ML Wed Aug 29 11:48:45 2012 +0200 @@ -130,7 +130,7 @@ fun position_of (Token ((_, (pos, _)), _, _)) = pos; fun end_position_of (Token ((_, (_, pos)), _, _)) = pos; -val pos_of = Position.str_of o position_of; +val pos_of = Position.here o position_of; (* control tokens *) @@ -244,7 +244,7 @@ fun put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files))) | put_files _ tok = - raise Fail ("Cannot put inlined files here" ^ Position.str_of (position_of tok)); + raise Fail ("Cannot put inlined files here" ^ Position.here (position_of tok)); (* access values *) @@ -402,7 +402,7 @@ fun read_antiq lex scan (syms, pos) = let - fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^ + fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^ "@{" ^ Symbol_Pos.content syms ^ "}"); val res = diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Isar/toplevel.ML Wed Aug 29 11:48:45 2012 +0200 @@ -189,8 +189,8 @@ | _ => raise UNDEF); fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy - | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.str_of pos) - | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos); + | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos) + | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos); (* print state *) @@ -359,7 +359,7 @@ fun print_of (Transition {print, ...}) = print; fun name_of (Transition {name, ...}) = name; fun pos_of (Transition {pos, ...}) = pos; -fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr); +fun str_of tr = quote (name_of tr) ^ Position.here (pos_of tr); fun command_msg msg tr = msg ^ "command " ^ str_of tr; fun at_command tr = command_msg "At " tr; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/ML/ml_antiquote.ML Wed Aug 29 11:48:45 2012 +0200 @@ -139,7 +139,7 @@ val res = (case try check (c, decl) of SOME res => res - | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos)); + | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); in ML_Syntax.print_string res end); val _ = Context.>> (Context.map_theory @@ -160,7 +160,7 @@ let val Const (c, _) = Proof_Context.read_const_proper ctxt false s; val res = check (Proof_Context.consts_of ctxt, c) - handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos); + handle TYPE (msg, _, _) => error (msg ^ Position.here pos); in ML_Syntax.print_string res end); val _ = Context.>> (Context.map_theory @@ -175,7 +175,7 @@ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) => if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) then ML_Syntax.print_string c - else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))) #> + else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #> inline (Binding.name "const") (Args.context -- Scan.lift Args.name_source -- Scan.optional @@ -197,14 +197,14 @@ fun with_keyword f = Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) => (f ((name, Thy_Header.the_keyword thy name), pos) - handle ERROR msg => error (msg ^ Position.str_of pos))); + handle ERROR msg => error (msg ^ Position.here pos))); val _ = Context.>> (Context.map_theory (value (Binding.name "keyword") (with_keyword (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name | ((name, SOME _), pos) => - error ("Expected minor keyword " ^ quote name ^ Position.str_of pos))) #> + error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #> value (Binding.name "command_spec") (with_keyword (fn ((name, SOME kind), pos) => @@ -217,7 +217,7 @@ (ML_Syntax.print_list ML_Syntax.print_string))) ML_Syntax.print_position) ((name, kind), pos)) | ((name, NONE), pos) => - error ("Expected command keyword " ^ quote name ^ Position.str_of pos))))); + error ("Expected command keyword " ^ quote name ^ Position.here pos))))); end; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/ML/ml_compiler_polyml.ML Wed Aug 29 11:48:45 2012 +0200 @@ -114,7 +114,7 @@ val pos = position_of loc; val txt = (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report) - ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^ + ((if hard then "Error" else "Warning") ^ Position.here pos ^ ":\n") ^ Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^ Position.reported_text pos Isabelle_Markup.report ""; in if hard then err txt else warn txt end; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/ML/ml_context.ML Wed Aug 29 11:48:45 2012 +0200 @@ -150,7 +150,7 @@ let val ctxt = (case opt_ctxt of - NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.str_of pos) + NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos) | SOME ctxt => Context.proof_of ctxt); val lex = #1 (Keyword.get_lexicons ()); diff -r 0350245dec1c -r 0518bf89c777 src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/ML/ml_env.ML Wed Aug 29 11:48:45 2012 +0200 @@ -85,7 +85,7 @@ val local_context: use_context = {tune_source = ML_Parse.fix_ints, name_space = name_space, - str_of_pos = Position.str_of oo Position.line_file, + str_of_pos = Position.here oo Position.line_file, print = writeln, error = error}; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/ML/ml_lex.ML Wed Aug 29 11:48:45 2012 +0200 @@ -82,7 +82,7 @@ Token (_, (Keyword, ":>")) => warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\ \prefer non-opaque matching (:) possibly with abstype" ^ - Position.str_of (pos_of tok)) + Position.here (pos_of tok)) | _ => ()); fun check_content_of tok = @@ -307,7 +307,7 @@ |> tap Antiquote.check_nesting |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ()))) handle ERROR msg => - cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos); + cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos); in input @ termination end; end; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/ML/ml_parse.ML --- a/src/Pure/ML/ml_parse.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/ML/ml_parse.ML Wed Aug 29 11:48:45 2012 +0200 @@ -18,7 +18,7 @@ fun !!! scan = let fun get_pos [] = " (end-of-input)" - | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok); + | get_pos (tok :: _) = Position.here (ML_Lex.pos_of tok); fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks) | err (toks, SOME msg) = (fn () => "SML syntax error" ^ get_pos toks ^ ": " ^ msg ()); @@ -67,7 +67,7 @@ val global_context: use_context = {tune_source = fix_ints, name_space = ML_Name_Space.global, - str_of_pos = Position.str_of oo Position.line_file, + str_of_pos = Position.here oo Position.line_file, print = writeln, error = error}; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Syntax/lexicon.ML Wed Aug 29 11:48:45 2012 +0200 @@ -298,7 +298,7 @@ (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of (toks, []) => toks | (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^ - Position.str_of (#1 (Symbol_Pos.range ss)))) + Position.here (#1 (Symbol_Pos.range ss)))) end; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Syntax/parser.ML Wed Aug 29 11:48:45 2012 +0200 @@ -702,7 +702,7 @@ [] => let val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata; - val pos = Position.str_of (Lexicon.pos_of_token prev_token); + val pos = Position.here (Lexicon.pos_of_token prev_token); in if null toks then error ("Inner syntax error: unexpected end of input" ^ pos) else error (Pretty.string_of (Pretty.block diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Aug 29 11:48:45 2012 +0200 @@ -142,7 +142,7 @@ let val pos = Lexicon.pos_of_token tok; val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok) - handle ERROR msg => error (msg ^ Position.str_of pos); + handle ERROR msg => error (msg ^ Position.here pos); val _ = report pos (markup_class ctxt) c; in [Ast.Constant (Lexicon.mark_class c)] end | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) = @@ -150,7 +150,7 @@ val pos = Lexicon.pos_of_token tok; val Type (c, _) = Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok) - handle ERROR msg => error (msg ^ Position.str_of pos); + handle ERROR msg => error (msg ^ Position.here pos); val _ = report pos (markup_type ctxt) c; in [Ast.Constant (Lexicon.mark_type c)] end | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) = @@ -268,7 +268,7 @@ | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x) | _ => if null ambig_msgs then - error ("Parse error: ambiguous syntax" ^ Position.str_of pos) + error ("Parse error: ambiguous syntax" ^ Position.here pos) else error (cat_lines ambig_msgs)); @@ -294,7 +294,7 @@ if len <= 1 then [] else [cat_lines - (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^ + (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^ "\nproduces " ^ string_of_int len ^ " parse trees" ^ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))]; @@ -379,7 +379,7 @@ Context_Position.if_visible ctxt warning (cat_lines (ambig_msgs @ ["Fortunately, only one parse tree is type correct" ^ - Position.str_of (Position.reset_range pos) ^ + Position.here (Position.reset_range pos) ^ ",\nbut you may still want to disambiguate your grammar or your input."])) else (); report_result ctxt pos [] results') else @@ -687,7 +687,7 @@ | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] = (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T] handle ERROR msg => - error (msg ^ Position.str_of (the_default Position.none (Term_Position.decode pos)))) + error (msg ^ Position.here (the_default Position.none (Term_Position.decode pos)))) | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts); diff -r 0350245dec1c -r 0518bf89c777 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/System/build.scala Wed Aug 29 11:48:45 2012 +0200 @@ -73,7 +73,7 @@ catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session entry " + - quote(entry.name) + Position.str_of(entry.pos)) + quote(entry.name) + Position.here(entry.pos)) } @@ -87,7 +87,7 @@ (Graph.string[Session_Info] /: infos) { case (graph, (name, info)) => if (graph.defined(name)) - error("Duplicate session " + quote(name) + Position.str_of(info.pos)) + error("Duplicate session " + quote(name) + Position.here(info.pos)) else graph.new_node(name, info) } val graph2 = @@ -98,7 +98,7 @@ case Some(parent) => if (!graph.defined(parent)) error("Bad parent session " + quote(parent) + " for " + - quote(name) + Position.str_of(info.pos)) + quote(name) + Position.here(info.pos)) try { graph.add_edge_acyclic(parent, name) } catch { @@ -106,7 +106,7 @@ error(cat_lines(exn.cycles.map(cycle => "Cyclic session dependency of " + cycle.map(c => quote(c.toString)).mkString(" via "))) + - Position.str_of(info.pos)) + Position.here(info.pos)) } } } @@ -374,7 +374,7 @@ catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session " + - quote(name) + Position.str_of(info.pos)) + quote(name) + Position.here(info.pos)) } val errors = parent_errors ::: thy_deps.deps.map(d => d._2.errors).flatten diff -r 0350245dec1c -r 0518bf89c777 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/System/options.scala Wed Aug 29 11:48:45 2012 +0200 @@ -77,7 +77,7 @@ case bad => error(bad.toString) } try { (options /: ops) { case (opts, op) => op(opts) } } - catch { case ERROR(msg) => error(msg + Position.str_of(file.position)) } + catch { case ERROR(msg) => error(msg + Position.here(file.position)) } } } diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Thy/rail.ML --- a/src/Pure/Thy/rail.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Thy/rail.ML Wed Aug 29 11:48:45 2012 +0200 @@ -35,7 +35,7 @@ fun print (Token ((pos, _), (k, x))) = (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^ - Position.str_of pos; + Position.here pos; fun print_keyword x = print_kind Keyword ^ " " ^ quote x; @@ -92,7 +92,7 @@ val prefix = "Rail syntax error"; fun get_pos [] = " (end-of-input)" - | get_pos (tok :: _) = Position.str_of (pos_of tok); + | get_pos (tok :: _) = Position.here (pos_of tok); fun err (toks, NONE) = (fn () => prefix ^ get_pos toks) | err (toks, SOME msg) = diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Thy/thy_header.ML Wed Aug 29 11:48:45 2012 +0200 @@ -140,7 +140,7 @@ in (case res of SOME (h, _) => h - | NONE => error ("Unexpected end of input" ^ Position.str_of pos)) + | NONE => error ("Unexpected end of input" ^ Position.here pos)) end; fun read pos str = read_source pos (token_source pos str); diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Thy/thy_info.ML Wed Aug 29 11:48:45 2012 +0200 @@ -274,7 +274,7 @@ val (current, deps, theory_pos, imports, uses, keywords) = check_deps dir' name handle ERROR msg => cat_error msg (loader_msg "the error(s) above occurred while examining theory" [name] ^ - Position.str_of require_pos ^ required_by "\n" initiators); + Position.here require_pos ^ required_by "\n" initiators); val parents = map (base_name o #1) imports; val (parents_current, tasks') = diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Thy/thy_load.ML Wed Aug 29 11:48:45 2012 +0200 @@ -109,7 +109,7 @@ Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks) => if Keyword.is_theory_load cmd then (case find_file toks of - NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.str_of pos) + NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos) | SOME (i, path) => let val toks' = toks |> map_index (fn (j, tok) => @@ -135,7 +135,7 @@ val {name = (name, pos), imports, uses, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_name <> name andalso - error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.str_of pos); + error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, uses = uses, keywords = keywords} diff -r 0350245dec1c -r 0518bf89c777 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/Thy/thy_output.ML Wed Aug 29 11:48:45 2012 +0200 @@ -110,7 +110,7 @@ in f src state ctxt handle ERROR msg => cat_error msg ("The error(s) above occurred in document antiquotation: " ^ - quote name ^ Position.str_of pos) + quote name ^ Position.here pos) end; fun option ((xname, pos), s) ctxt = @@ -198,7 +198,7 @@ val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); in if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then - error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos) + error ("Unknown context -- cannot expand document antiquotations" ^ Position.here pos) else implode (map expand ants) end; @@ -309,7 +309,7 @@ else (case drop (~ nesting - 1) tags of tgs :: tgss => (tgs, tgss) - | [] => err_bad_nesting (Position.str_of cmd_pos)); + | [] => err_bad_nesting (Position.here cmd_pos)); val buffer' = buffer @@ -535,7 +535,7 @@ fun pretty_theory ctxt (name, pos) = (case find_first (fn thy => Context.theory_name thy = name) (Theory.nodes_of (Proof_Context.theory_of ctxt)) of - NONE => error ("No ancestor theory " ^ quote name ^ Position.str_of pos) + NONE => error ("No ancestor theory " ^ quote name ^ Position.here pos) | SOME thy => (Position.report pos (Theory.get_markup thy); Pretty.str name)); diff -r 0350245dec1c -r 0518bf89c777 src/Pure/consts.ML --- a/src/Pure/consts.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/consts.ML Wed Aug 29 11:48:45 2012 +0200 @@ -146,7 +146,7 @@ fun read_const consts (raw_c, pos) = let val c = intern consts raw_c; - val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos); + val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos); in Const (c, T) end; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/context.ML --- a/src/Pure/context.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/context.ML Wed Aug 29 11:48:45 2012 +0200 @@ -135,7 +135,7 @@ (case Datatab.lookup (Synchronized.value kinds) k of SOME kind => if ! timing andalso name <> "" then - Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.str_of (#pos kind)) + Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind)) (fn () => f kind x) else f kind x | NONE => raise Fail "Invalid theory data identifier"); diff -r 0350245dec1c -r 0518bf89c777 src/Pure/facts.ML --- a/src/Pure/facts.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/facts.ML Wed Aug 29 11:48:45 2012 +0200 @@ -100,7 +100,7 @@ val n = length ths; fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^ - Position.str_of pos); + Position.here pos); fun sel i = if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i) else nth ths (i - 1); diff -r 0350245dec1c -r 0518bf89c777 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/global_theory.ML Wed Aug 29 11:48:45 2012 +0200 @@ -103,7 +103,7 @@ val _ = Theory.check_thy thy; in (case res of - NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos) + NONE => error ("Unknown fact " ^ quote name ^ Position.here pos) | SOME (static, ths) => (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name); if static then () diff -r 0350245dec1c -r 0518bf89c777 src/Pure/goal.ML --- a/src/Pure/goal.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/goal.ML Wed Aug 29 11:48:45 2012 +0200 @@ -208,7 +208,7 @@ fun err msg = cat_error msg ("The error(s) above occurred for the goal statement:\n" ^ string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^ - (case Position.str_of pos of "" => "" | s => "\n" ^ s)); + (case Position.here pos of "" => "" | s => "\n" ^ s)); fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t)) handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/raw_simplifier.ML Wed Aug 29 11:48:45 2012 +0200 @@ -1057,7 +1057,7 @@ val _ = if b <> b' then warning ("Simplifier: renamed bound variable " ^ - quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ())) + quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ())) else (); val ss' = add_bound ((b', T), a) ss; val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0; diff -r 0350245dec1c -r 0518bf89c777 src/Pure/type.ML --- a/src/Pure/type.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/type.ML Wed Aug 29 11:48:45 2012 +0200 @@ -258,7 +258,7 @@ fun the_decl tsig (c, pos) = (case lookup_type tsig c of - NONE => error (undecl_type c ^ Position.str_of pos) + NONE => error (undecl_type c ^ Position.here pos) | SOME decl => decl); diff -r 0350245dec1c -r 0518bf89c777 src/Tools/WWW_Find/unicode_symbols.ML --- a/src/Tools/WWW_Find/unicode_symbols.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Tools/WWW_Find/unicode_symbols.ML Wed Aug 29 11:48:45 2012 +0200 @@ -109,7 +109,7 @@ (toks, []) => toks | (_, ss) => error ("Lexical error at: " ^ Symbol_Pos.content ss ^ - Position.str_of (#1 (Symbol_Pos.range ss)))) + Position.here (#1 (Symbol_Pos.range ss)))) end; val stopper = @@ -152,8 +152,8 @@ Symtab.update_new (abbr, uni) fromabbr, Inttab.update (uni, sym) tosym, Inttab.update (uni, abbr) toabbr)) - handle Symtab.DUP sym => error ("Duplicate at" ^ Position.str_of pos) - | Inttab.DUP sym => error ("Duplicate code at" ^ Position.str_of pos); + handle Symtab.DUP sym => error ("Duplicate at" ^ Position.here pos) + | Inttab.DUP sym => error ("Duplicate code at" ^ Position.here pos); in diff -r 0350245dec1c -r 0518bf89c777 src/Tools/induct_tacs.ML --- a/src/Tools/induct_tacs.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Tools/induct_tacs.ML Wed Aug 29 11:48:45 2012 +0200 @@ -23,7 +23,7 @@ val u = singleton (Variable.polymorphic ctxt) t; val U = Term.fastype_of u; val _ = Term.is_TVar U andalso - error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u ^ Position.str_of pos); + error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u ^ Position.here pos); in (u, U) end; fun gen_case_tac ctxt0 s opt_rule i st = @@ -75,17 +75,17 @@ val pos = Syntax.read_token_pos name; val (x, _) = Term.dest_Free t handle TERM _ => error ("Induction argument not a variable: " ^ - Syntax.string_of_term ctxt t ^ Position.str_of pos); + Syntax.string_of_term ctxt t ^ Position.here pos); val eq_x = fn Free (y, _) => x = y | _ => false; val _ = if Term.exists_subterm eq_x concl then () else error ("No such variable in subgoal: " ^ - Syntax.string_of_term ctxt t ^ Position.str_of pos); + Syntax.string_of_term ctxt t ^ Position.here pos); val _ = if (exists o Term.exists_subterm) eq_x prems then warning ("Induction variable occurs also among premises: " ^ - Syntax.string_of_term ctxt t ^ Position.str_of pos) + Syntax.string_of_term ctxt t ^ Position.here pos) else (); in #1 (check_type ctxt (t, pos)) end;