# HG changeset patch # User wenzelm # Date 1232115605 -3600 # Node ID 53bda11e0d3bfbeb1cd0255d9fde1a780b57d0e1 # Parent b0e01a48867c5a2724fdcf4a70a976ea6024b0f6 export check_name; diff -r b0e01a48867c -r 53bda11e0d3b src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Fri Jan 16 12:11:06 2009 +0100 +++ b/src/Pure/Thy/thy_load.ML Fri Jan 16 15:20:05 2009 +0100 @@ -25,6 +25,7 @@ val check_file: Path.T -> Path.T -> (Path.T * File.ident) option val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option val check_thy: Path.T -> string -> Path.T * File.ident + val check_name: string -> string -> unit val deps_thy: Path.T -> string -> {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list} val load_ml: Path.T -> Path.T -> Path.T * File.ident @@ -95,6 +96,11 @@ | SOME thy_id => thy_id) end; +fun check_name name name' = + if name = name' then () + else error ("Filename " ^ quote (Path.implode (thy_path name)) ^ + " does not agree with theory name " ^ quote name'); + (* theory deps *) @@ -104,9 +110,7 @@ val text = explode (File.read path); val (name', imports, uses) = 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'); + val _ = check_name name name'; val uses = map (Path.explode o #1) uses; in {master = master, text = text, imports = imports, uses = uses} end;