src/Pure/Thy/thy_syn.ML
changeset 6231 438a642ee92d
parent 6206 7d2204fcc1e5
child 6641 254ab03bd082
equal deleted inserted replaced
6230:85fc589a66ea 6231:438a642ee92d
    53   let
    53   let
    54     val tmp_path = File.tmp_path (ThyLoad.ml_path (name ^ "_thy"));
    54     val tmp_path = File.tmp_path (ThyLoad.ml_path (name ^ "_thy"));
    55     val txt_out = ThyParse.parse_thy (! syntax) chs;
    55     val txt_out = ThyParse.parse_thy (! syntax) chs;
    56   in
    56   in
    57     File.write tmp_path txt_out;
    57     File.write tmp_path txt_out;
    58     Use.use_path tmp_path;
    58     Symbol.use tmp_path;
    59     if ! delete_tmpfiles then File.rm tmp_path else ()
    59     if ! delete_tmpfiles then File.rm tmp_path else ()
    60   end;
    60   end;
    61 
    61 
    62 
    62 
    63 end;
    63 end;