# HG changeset patch
# User wenzelm
# Date 1210755908 -7200
# Node ID bb68f50644a9f1f5c583aad55b68e54efe1dd7c8
# Parent  ebcd5c23dd961567afe9353428a646f40ca0c8e6
renamed Position.path to Path.position;

diff -r ebcd5c23dd96 -r bb68f50644a9 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed May 14 11:05:07 2008 +0200
+++ b/src/Pure/General/path.ML	Wed May 14 11:05:08 2008 +0200
@@ -26,6 +26,7 @@
   val ext: string -> T -> T
   val split_ext: T -> T * string
   val expand: T -> T
+  val position: T -> Position.T
 end;
 
 structure Path: PATH =
@@ -153,6 +154,11 @@
 val expand = rep #> maps eval #> norm #> Path;
 
 
+(* source position *)
+
+val position = Position.file o implode_path o expand;
+
+
 (*final declarations of this structure!*)
 val implode = implode_path;
 val explode = explode_path;
diff -r ebcd5c23dd96 -r bb68f50644a9 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed May 14 11:05:07 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed May 14 11:05:08 2008 +0200
@@ -234,7 +234,7 @@
 fun process_file path thy =
   let
     val result = ref thy;
-    val trs = parse (Position.path path) (File.read path);
+    val trs = parse (Path.position path) (File.read path);
     val init = Toplevel.init_theory (K thy) (fn thy' => result := thy') (K ());
     val _ = Toplevel.excursion (init Toplevel.empty :: trs @ [Toplevel.exit Toplevel.empty]);
   in ! result end;
diff -r ebcd5c23dd96 -r bb68f50644a9 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed May 14 11:05:07 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Wed May 14 11:05:08 2008 +0200
@@ -187,7 +187,7 @@
 (* ML evaluation *)
 
 val eval = eval_wrapper Output.ml_output;
-fun eval_file path = eval true (Position.path path) (File.read path);
+fun eval_file path = eval true (Path.position path) (File.read path);
 
 fun eval_in context verbose pos txt =
   Context.setmp_thread_data context (fn () => eval verbose pos txt) ();
diff -r ebcd5c23dd96 -r bb68f50644a9 src/Pure/Thy/thy_edit.ML
--- a/src/Pure/Thy/thy_edit.ML	Wed May 14 11:05:07 2008 +0200
+++ b/src/Pure/Thy/thy_edit.ML	Wed May 14 11:05:08 2008 +0200
@@ -116,7 +116,7 @@
 (* HTML presentation -- example *)
 
 fun present_html inpath outpath =
-  Source.exhaust (item_source (Position.path inpath) (Source.of_string (File.read inpath)))
+  Source.exhaust (item_source (Path.position inpath) (Source.of_string (File.read inpath)))
   |> HTML.html_mode (implode o map present_item)
   |> enclose
     (HTML.begin_document (Path.implode (Path.base inpath)) ^ "<div class=\"source\"><pre>")
diff -r ebcd5c23dd96 -r bb68f50644a9 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed May 14 11:05:07 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed May 14 11:05:08 2008 +0200
@@ -307,7 +307,7 @@
     val (pos, text, files) =
       (case get_deps name of
         SOME {master = SOME (master_path, _), text as _ :: _, files, ...} =>
-          (Position.path master_path, text, files)
+          (Path.position master_path, text, files)
       | _ => error (loader_msg "corrupted dependency information" [name]));
     val _ = touch_thy name;
     val _ = CRITICAL (fn () =>
diff -r ebcd5c23dd96 -r bb68f50644a9 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed May 14 11:05:07 2008 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed May 14 11:05:08 2008 +0200
@@ -98,7 +98,7 @@
     val master as (path, _) = check_thy dir name;
     val text = explode (File.read path);
     val (name', imports, uses) =
-      ThyHeader.read (Position.path path) (Source.of_list_limited 8000 text);
+      ThyHeader.read (Path.position path) (Source.of_list_limited 8000 text);
     val _ = name = name' orelse
       error ("Filename " ^ quote (Path.implode (Path.base path)) ^
         " does not agree with theory name " ^ quote name');