src/Pure/Thy/thy_syn.ML
changeset 6641 254ab03bd082
parent 6231 438a642ee92d
child 7024 44bd3c094fd6
equal deleted inserted replaced
6640:d2e8342bf5c3 6641:254ab03bd082
    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     Symbol.use tmp_path;
    58     File.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;