tuned signature;
authorwenzelm
Thu Jul 22 20:36:41 2010 +0200 (2010-07-22 ago)
changeset 379379e482a3e651e
parent 37936 1e4c5015a72e
child 37938 445e5a3244cc
tuned signature;
src/Pure/Isar/toplevel.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jul 22 18:08:39 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jul 22 20:36:41 2010 +0200
     1.3 @@ -632,7 +632,7 @@
     1.4  fun run_command thy_name tr st =
     1.5    (case
     1.6        (case init_of tr of
     1.7 -        SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
     1.8 +        SOME name => Exn.capture (fn () => Thy_Load.consistent_name thy_name name) ()
     1.9        | NONE => Exn.Result ()) of
    1.10      Exn.Result () =>
    1.11        let val int = is_some (init_of tr) in
     2.1 --- a/src/Pure/Thy/thy_load.ML	Thu Jul 22 18:08:39 2010 +0200
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Thu Jul 22 20:36:41 2010 +0200
     2.3 @@ -22,10 +22,10 @@
     2.4    val ml_path: string -> Path.T
     2.5    val thy_path: string -> Path.T
     2.6    val split_thy_path: Path.T -> Path.T * string
     2.7 +  val consistent_name: string -> string -> unit
     2.8    val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
     2.9    val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
    2.10    val check_thy: Path.T -> string -> Path.T * File.ident
    2.11 -  val check_name: string -> string -> unit
    2.12    val deps_thy: Path.T -> string ->
    2.13     {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
    2.14    val load_ml: Path.T -> Path.T -> Path.T * File.ident
    2.15 @@ -75,6 +75,11 @@
    2.16      (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
    2.17    | _ => error ("Bad theory file specification " ^ Path.implode path));
    2.18  
    2.19 +fun consistent_name name name' =
    2.20 +  if name = name' then ()
    2.21 +  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
    2.22 +    " does not agree with theory name " ^ quote name');
    2.23 +
    2.24  
    2.25  (* check files *)
    2.26  
    2.27 @@ -103,11 +108,6 @@
    2.28      | SOME thy_id => thy_id)
    2.29    end;
    2.30  
    2.31 -fun check_name name name' =
    2.32 -  if name = name' then ()
    2.33 -  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
    2.34 -    " does not agree with theory name " ^ quote name');
    2.35 -
    2.36  
    2.37  (* theory deps *)
    2.38  
    2.39 @@ -117,7 +117,7 @@
    2.40      val text = File.read path;
    2.41      val (name', imports, uses) =
    2.42        Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
    2.43 -    val _ = check_name name name';
    2.44 +    val _ = consistent_name name name';
    2.45      val uses = map (Path.explode o #1) uses;
    2.46    in {master = master, text = text, imports = imports, uses = uses} end;
    2.47