# HG changeset patch # User wenzelm # Date 1237851052 -3600 # Node ID 0863bb353065a23ecd80a6653c77b5a1e4540a39 # Parent bcc63fcbc3ce4fd33e81a93b95f7d0eddab9fc2f more systematic type use_context; result_fun: actually apply result, only one version of eval; removed obsolete 'ML_parse'; diff -r bcc63fcbc3ce -r 0863bb353065 src/Pure/ML/ml_test.ML --- a/src/Pure/ML/ml_test.ML Mon Mar 23 22:57:27 2009 +0100 +++ b/src/Pure/ML/ml_test.ML Tue Mar 24 00:30:52 2009 +0100 @@ -7,7 +7,7 @@ signature ML_TEST = sig val get_result: Proof.context -> PolyML.parseTree list - val eval: bool -> bool -> Position.T -> ML_Lex.token list -> unit + val eval: bool -> Position.T -> ML_Lex.token list -> unit end structure ML_Test: ML_TEST = @@ -25,8 +25,11 @@ val get_result = Result.get o Context.Proof; -fun eval do_run verbose pos toks = + +fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks = let + (* input *) + val input = toks |> map (fn tok => (serial (), (String.explode (ML_Lex.text_of tok), ML_Lex.pos_of tok))); val index_pos = Inttab.lookup (Inttab.make (map (apsnd snd) input)); @@ -49,50 +52,106 @@ SOME c)); fun get_index () = (case ! in_buffer of [] => 0 | (i, _) :: _ => i); + + (* output *) + val out_buffer = ref ([]: string list); + fun output () = implode (rev (! out_buffer)); fun put s = out_buffer := s :: ! out_buffer; - fun output () = implode (rev (! out_buffer)); fun put_message {message, hard, location, context = _} = (put (if hard then "Error: " else "Warning: "); put (Pretty.string_of (Pretty.from_ML (pretty_ml message))); put (Position.str_of (pos_of location) ^ "\n")); + + (* results *) + + fun apply_result {fixes, types, signatures, structures, functors, values} = + let + fun add_prefix prefix (PrettyBlock (ind, consistent, context, prts)) = + let + fun make_prefix context = + (case get_first (fn ContextParentStructure p => SOME p | _ => NONE) context of + SOME (name, sub_context) => make_prefix sub_context ^ name ^ "." + | NONE => prefix); + val this_prefix = make_prefix context; + in PrettyBlock (ind, consistent, context, map (add_prefix this_prefix) prts) end + | add_prefix prefix (prt as PrettyString s) = + if prefix = "" then prt else PrettyString (prefix ^ s) + | add_prefix _ (prt as PrettyBreak _) = prt; + + val depth = get_print_depth (); + val with_struct = ! PolyML.Compiler.printTypesWithStructureName; + + fun display disp x = + if depth > 0 then + (disp x + |> with_struct ? add_prefix "" + |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n") + else (); + + fun apply_fix (a, b) = + (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b)); + fun apply_type (a, b) = + (display PolyML.NameSpace.displayType (b, depth); #enterType space (a, b)); + fun apply_sig (a, b) = + (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b)); + fun apply_struct (a, b) = + (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b)); + fun apply_funct (a, b) = + (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b)); + fun apply_val (a, b) = + (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b)); + in + List.app apply_fix fixes; + List.app apply_type types; + List.app apply_sig signatures; + List.app apply_struct structures; + List.app apply_funct functors; + List.app apply_val values + end; + fun result_fun (parse_tree, code) () = (Context.>> (Result.map (append (the_list parse_tree))); - if is_none code then warning "Static Errors" else ()); + (case code of NONE => warning "Static Errors" | SOME result => apply_result (result ()))); + + + (* compiler invocation *) val parameters = [PolyML.Compiler.CPOutStream put, - PolyML.Compiler.CPNameSpace ML_Context.name_space, + PolyML.Compiler.CPNameSpace space, PolyML.Compiler.CPErrorMessageProc put_message, PolyML.Compiler.CPLineNo (fn () => ! current_line), PolyML.Compiler.CPLineOffset get_index, PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)), - PolyML.Compiler.CPPrintInAlphabeticalOrder false] @ - (if do_run then [] else [PolyML.Compiler.CPCompilerResultFun result_fun]); + PolyML.Compiler.CPPrintInAlphabeticalOrder false, + PolyML.Compiler.CPCompilerResultFun result_fun]; val _ = (while not (List.null (! in_buffer)) do PolyML.compiler (get, parameters) ()) handle exn => (put ("Exception- " ^ General.exnMessage exn ^ " raised"); error (output ()); raise exn); - in if verbose then writeln (output ()) else () end; + in if verbose then print (output ()) else () end; + +val eval = use_text ML_Context.local_context; (* ML test command *) -fun ML_test do_run (txt, pos) = +fun ML_test (txt, pos) = let val _ = Position.report Markup.ML_source pos; val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos); val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ()); val _ = Context.setmp_thread_data env_ctxt - (fn () => (eval true false Position.none env; Context.thread_data ())) () + (fn () => (eval false Position.none env; Context.thread_data ())) () |> (fn NONE => () | SOME context' => Context.>> (ML_Context.inherit_env context')); - val _ = eval do_run true pos body; - val _ = eval true false Position.none (ML_Lex.tokenize "structure Isabelle = struct end"); + val _ = eval true pos body; + val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end"); in () end; @@ -105,12 +164,7 @@ val _ = OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl) (P.ML_source >> (fn src => - Toplevel.generic_theory (ML_Context.exec (fn () => ML_test true src) #> inherit_env))); - -val _ = - OuterSyntax.command "ML_parse" "advanced ML compiler test (parse only)" (K.tag_ml K.thy_decl) - (P.ML_source >> (fn src => - Toplevel.generic_theory (ML_Context.exec (fn () => ML_test false src) #> inherit_env))); + Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> inherit_env))); end;