unique file names via serial numbers, to allow files like "root" or multiple files with same base name;
authorwenzelm
Mon Sep 19 14:31:20 2011 +0200 (2011-09-19)
changeset 449866f27ecf2a951
parent 44985 272e8e4e4fc7
child 44987 fd3a36e48b09
unique file names via serial numbers, to allow files like "root" or multiple files with same base name;
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/present.ML	Mon Sep 19 12:58:52 2011 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Mon Sep 19 14:31:20 2011 +0200
     1.3 @@ -499,8 +499,8 @@
     1.4          val base = Path.base path;
     1.5          val name =
     1.6            (case Path.implode (#1 (Path.split_ext base)) of
     1.7 -            "" => "DUMMY" ^ serial_string ()
     1.8 -          | s => s);
     1.9 +            "" => "DUMMY"
    1.10 +          | s => s)  ^ serial_string ();
    1.11        in
    1.12          if File.exists path then
    1.13            (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)