--- 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
--- 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
--- 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) ^
--- 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)
--- 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;
--- 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 ()
--- 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 =
--- 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 =
--- 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) + ")"
--- 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 ^
--- 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;
--- 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
--- 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;
--- 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 =>
--- 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 =
--- 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
--- 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 ?!? *)
--- 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 =
--- 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;
--- 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;
--- 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;
--- 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 ());
--- 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};
--- 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;
--- 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};
--- 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;
--- 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
--- 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);
--- 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
--- 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)) }
}
}
--- 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) =
--- 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);
--- 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') =
--- 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}
--- 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));
--- 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;
--- 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");
--- 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);
--- 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 ()
--- 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;
--- 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;
--- 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);
--- 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
--- 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;