comparison src/compiler.sml @ 2241:2b1af5dc6dee

Merge.
author Ziv Scully <ziv@mit.edu>
date Sun, 19 Jul 2015 19:05:16 -0700
parents e10881cd92da 8c81cd351c1a
children f8903af753ff
comparison
equal deleted inserted replaced
2240:88cc0f44c940 2241:2b1af5dc6dee
873 873
874 | "file" => 874 | "file" =>
875 (case String.fields Char.isSpace arg of 875 (case String.fields Char.isSpace arg of
876 [uri, fname] => (Settings.setFilePath thisPath; 876 [uri, fname] => (Settings.setFilePath thisPath;
877 Settings.addFile {Uri = uri, 877 Settings.addFile {Uri = uri,
878 LoadFromFilename = fname}) 878 LoadFromFilename = fname};
879 url := {action = Settings.Allow, kind = Settings.Exact, pattern = uri} :: !url)
879 | _ => ErrorMsg.error "Bad 'file' arguments") 880 | _ => ErrorMsg.error "Bad 'file' arguments")
880 881
881 | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'"); 882 | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'");
882 read () 883 read ()
883 end 884 end