# HG changeset patch
# User wenzelm
# Date 1279999341 -7200
# Node ID bc285d91041ec5b17f6ff4f8c8f39d088a2c8e08
# Parent  48a8744441648d40135db2a5fd931e6cb3075ce8
moved basic thy file name operations from Thy_Load to Thy_Header;

diff -r 48a874444164 -r bc285d91041e src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Sat Jul 24 12:14:53 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Sat Jul 24 21:22:21 2010 +0200
@@ -181,7 +181,7 @@
 
 fun begin_document (id: document_id) path =
   let
-    val (dir, name) = Thy_Load.split_thy_path path;
+    val (dir, name) = Thy_Header.split_thy_path path;
     val _ = define_document id (make_document dir name no_entries);
   in () end;
 
diff -r 48a874444164 -r bc285d91041e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Jul 24 12:14:53 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Jul 24 21:22:21 2010 +0200
@@ -629,7 +629,7 @@
 fun run_command thy_name tr st =
   (case
       (case init_of tr of
-        SOME name => Exn.capture (fn () => Thy_Load.consistent_name thy_name name) ()
+        SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
       | NONE => Exn.Result ()) of
     Exn.Result () =>
       let val int = is_some (init_of tr) in
diff -r 48a874444164 -r bc285d91041e src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jul 24 12:14:53 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jul 24 21:22:21 2010 +0200
@@ -142,7 +142,7 @@
             Thy_Info.touch_child_thys name; Thy_Info.register_thy name)
           handle ERROR msg =>
             (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
-              tell_file_retracted (Thy_Load.thy_path name))
+              tell_file_retracted (Thy_Header.thy_path name))
       else ();
     val _ = Isar.init ();
   in () end;
diff -r 48a874444164 -r bc285d91041e src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sat Jul 24 12:14:53 2010 +0200
+++ b/src/Pure/Thy/thy_header.ML	Sat Jul 24 21:22:21 2010 +0200
@@ -8,6 +8,9 @@
 sig
   val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
   val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
+  val thy_path: string -> Path.T
+  val split_thy_path: Path.T -> Path.T * string
+  val consistent_name: string -> string -> unit
 end;
 
 structure Thy_Header: THY_HEADER =
@@ -63,4 +66,19 @@
     | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
   end;
 
+
+(* file formats *)
+
+val thy_path = Path.ext "thy" o Path.basic;
+
+fun split_thy_path path =
+  (case Path.split_ext path of
+    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
+  | _ => error ("Bad theory file specification " ^ Path.implode path));
+
+fun consistent_name name name' =
+  if name = name' then ()
+  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
+    " does not agree with theory name " ^ quote name');
+
 end;
diff -r 48a874444164 -r bc285d91041e src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sat Jul 24 12:14:53 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Sat Jul 24 21:22:21 2010 +0200
@@ -21,10 +21,6 @@
   val init: Path.T -> theory -> theory
   val require: Path.T -> theory -> theory
   val provide: Path.T * (Path.T * File.ident) -> theory -> theory
-  val ml_path: string -> Path.T
-  val thy_path: string -> Path.T
-  val split_thy_path: Path.T -> Path.T * string
-  val consistent_name: string -> string -> unit
   val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_file: Path.T -> Path.T -> Path.T * File.ident
   val check_thy: Path.T -> string -> Path.T * File.ident
@@ -105,22 +101,6 @@
 end;
 
 
-(* file formats *)
-
-val ml_path = Path.ext "ML" o Path.basic;
-val thy_path = Path.ext "thy" o Path.basic;
-
-fun split_thy_path path =
-  (case Path.split_ext path of
-    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
-  | _ => error ("Bad theory file specification " ^ Path.implode path));
-
-fun consistent_name name name' =
-  if name = name' then ()
-  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
-    " does not agree with theory name " ^ quote name');
-
-
 (* check files *)
 
 local
@@ -152,7 +132,7 @@
     error ("Could not find file " ^ quote (Path.implode path) ^
       "\nin " ^ commas_quote (map Path.implode prfxs));
 
-fun check_thy dir name = check_file dir (thy_path name);
+fun check_thy dir name = check_file dir (Thy_Header.thy_path name);
 
 end;
 
@@ -165,7 +145,7 @@
     val text = File.read path;
     val (name', imports, uses) =
       Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
-    val _ = consistent_name name name';
+    val _ = Thy_Header.consistent_name name name';
     val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;
 
diff -r 48a874444164 -r bc285d91041e src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Sat Jul 24 12:14:53 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Sat Jul 24 21:22:21 2010 +0200
@@ -173,7 +173,8 @@
       end
   | process (code_body, _) _ (SOME file_name) thy =
       let
-        val preamble = "(* Generated from " ^ Path.implode (Thy_Load.thy_path (Context.theory_name thy))
+        val preamble =
+          "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
           ^ "; DO NOT EDIT! *)";
         val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
       in