src/Pure/Thy/present.ML
changeset 24829 e1214fa781ca
parent 24561 7b4aa14d2491
child 26323 73efc70edeef
equal deleted inserted replaced
24828:137c242e7277 24829:e1214fa781ca
   531   let
   531   let
   532     fun prep_draft path i =
   532     fun prep_draft path i =
   533       let
   533       let
   534         val base = Path.base path;
   534         val base = Path.base path;
   535         val name =
   535         val name =
   536           (case Path.implode (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
   536           (case Path.implode (#1 (Path.split_ext base)) of
       
   537             "" => "DUMMY" ^ serial_string ()
       
   538           | s => s);
   537       in
   539       in
   538         if File.exists path then
   540         if File.exists path then
   539           (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
   541           (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
   540         else error ("Bad file: " ^ quote (Path.implode path))
   542         else error ("Bad file: " ^ quote (Path.implode path))
   541       end;
   543       end;