# HG changeset patch
# User wenzelm
# Date 1393233449 -3600
# Node ID f4b114070675be8f4ab922dffe21892f28ad698e
# Parent  064c7c249f551b9b70ffd32e5a6316ec57c11e0a
tuned signature;

diff -r 064c7c249f55 -r f4b114070675 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/Pure/Isar/args.ML	Mon Feb 24 10:17:29 2014 +0100
@@ -191,7 +191,7 @@
 
 fun named_attribute att =
   internal_attribute ||
-  named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.position_of tok));
+  named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
 
 
 (* terms and types *)
diff -r 064c7c249f55 -r f4b114070675 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/Pure/Isar/method.ML	Mon Feb 24 10:17:29 2014 +0100
@@ -408,7 +408,7 @@
  (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
   (* FIXME implicit "cartouche" method (experimental, undocumented) *)
   Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
-    Source (Args.src (("cartouche", [tok]), Token.position_of tok))) ||
+    Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) ||
   Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
 and meth3 x =
  (meth4 --| Parse.$$$ "?" >> Try ||
diff -r 064c7c249f55 -r f4b114070675 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Feb 24 10:17:29 2014 +0100
@@ -310,7 +310,7 @@
     let val name = Token.content_of tok in
       (case lookup_commands outer_syntax name of
         NONE => []
-      | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
+      | SOME cmd => [((Token.pos_of tok, command_markup false (name, cmd)), "")])
     end
   else [];
 
diff -r 064c7c249f55 -r f4b114070675 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/Pure/Isar/parse.ML	Mon Feb 24 10:17:29 2014 +0100
@@ -122,9 +122,11 @@
         (fn () =>
           (case Token.text_of tok of
             (txt, "") =>
-              s () ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
+              s () ^ " expected,\nbut " ^ txt ^ Position.here (Token.pos_of tok) ^
+              " was found"
           | (txt1, txt2) =>
-              s () ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
+              s () ^ " expected,\nbut " ^ txt1 ^ Position.here (Token.pos_of tok) ^
+              " was found:\n" ^ txt2)));
 
 
 (* cut *)
@@ -132,7 +134,7 @@
 fun cut kind scan =
   let
     fun get_pos [] = " (end-of-input)"
-      | get_pos (tok :: _) = Token.pos_of tok;
+      | get_pos (tok :: _) = Position.here (Token.pos_of tok);
 
     fun err (toks, NONE) = (fn () => kind ^ get_pos toks)
       | err (toks, SOME msg) =
@@ -165,7 +167,7 @@
 
 val not_eof = RESET_VALUE (Scan.one Token.not_eof);
 
-fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
+fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap;
 fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
 fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
 
diff -r 064c7c249f55 -r f4b114070675 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/Pure/Isar/token.ML	Mon Feb 24 10:17:29 2014 +0100
@@ -16,10 +16,8 @@
     Attribute of morphism -> attribute | Files of file Exn.result list
   type T
   val str_of_kind: kind -> string
-  val position_of: T -> Position.T
-  val end_position_of: T -> Position.T
+  val pos_of: T -> Position.T
   val position_range_of: T list -> Position.range
-  val pos_of: T -> string
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -130,13 +128,11 @@
 
 (* position *)
 
-fun position_of (Token ((_, (pos, _)), _, _)) = pos;
-fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
+fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
+fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
 
 fun position_range_of [] = Position.no_range
-  | position_range_of toks = (position_of (hd toks), end_position_of (List.last toks));
-
-val pos_of = Position.here o position_of;
+  | position_range_of toks = (pos_of (hd toks), end_pos_of (List.last toks));
 
 
 (* control tokens *)
@@ -153,7 +149,7 @@
   | not_sync _ = true;
 
 val stopper =
-  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
 
 
 (* kind of token *)
@@ -251,8 +247,7 @@
 
 fun put_files [] tok = tok
   | 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.here (position_of tok));
+  | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok));
 
 
 (* access values *)
diff -r 064c7c249f55 -r f4b114070675 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Mon Feb 24 10:17:29 2014 +0100
@@ -132,7 +132,7 @@
       Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
     val pos =
       (case find_first Token.is_command span of
-        SOME tok => Token.position_of tok
+        SOME tok => Token.pos_of tok
       | NONE => proper_range);
 
     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
diff -r 064c7c249f55 -r f4b114070675 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML	Mon Feb 24 10:17:29 2014 +0100
@@ -85,7 +85,7 @@
       [] =>
         let
           val master_dir = master_directory thy;
-          val pos = Token.position_of tok;
+          val pos = Token.pos_of tok;
           val src_paths = Keyword.command_files cmd (Path.explode name);
         in map (Command.read_file master_dir pos) src_paths end
     | files => map Exn.release files));
diff -r 064c7c249f55 -r f4b114070675 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Mon Feb 24 00:04:48 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Mon Feb 24 10:17:29 2014 +0100
@@ -86,7 +86,7 @@
           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
     val (markup, txt) = token_markup tok;
-    val reports = ((Token.position_of tok, markup), txt) :: malformed_symbols;
+    val reports = ((Token.pos_of tok, markup), txt) :: malformed_symbols;
   in (is_malformed, reports) end;
 
 in
@@ -121,7 +121,7 @@
 
 fun make_span toks =
   if not (null toks) andalso Token.is_command (hd toks) then
-    Span (Command (Token.content_of (hd toks), Token.position_of (hd toks)), toks)
+    Span (Command (Token.content_of (hd toks), Token.pos_of (hd toks)), toks)
   else if forall Token.is_improper toks then Span (Ignored, toks)
   else Span (Malformed, toks);
 
@@ -162,8 +162,8 @@
       if Token.is_command tok then
         toks |> get_first (fn (i, tok) =>
           if Token.is_name tok then
-            SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
-              handle ERROR msg => error (msg ^ Token.pos_of tok)
+            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
+              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
           else NONE)
       else NONE
   | find_file [] = NONE;