1(* Title: Pure/ML/ml_file.ML 2 Author: Makarius 3 4Commands to load ML files. 5*) 6 7signature ML_FILE = 8sig 9 val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition 10 val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition 11end; 12 13structure ML_File: ML_FILE = 14struct 15 16fun command SML debug files = Toplevel.generic_theory (fn gthy => 17 let 18 val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy); 19 val provide = Resources.provide (src_path, digest); 20 val source = Input.source true (cat_lines lines) (pos, pos); 21 22 val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source); 23 24 val flags = 25 {SML = SML, exchange = false, redirect = true, verbose = true, 26 debug = debug, writeln = writeln, warning = warning}; 27 in 28 gthy 29 |> ML_Context.exec (fn () => ML_Context.eval_source flags source) 30 |> Local_Theory.propagate_ml_env 31 |> Context.mapping provide (Local_Theory.background_theory provide) 32 end); 33 34val ML = command false; 35val SML = command true; 36 37end; 38