# HG changeset patch # User wenzelm # Date 1337866425 -7200 # Node ID c81801f881b346077482d12f69771ae796b86ed1 # Parent 59ec72d3d0b9b87c70d824581ad88395852a9768 simplified Poly/ML setup -- 5.3.0 is now the common base-line; diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/General/linear_set.ML --- a/src/Pure/General/linear_set.ML Thu May 24 15:01:17 2012 +0200 +++ b/src/Pure/General/linear_set.ML Thu May 24 15:33:45 2012 +0200 @@ -133,7 +133,7 @@ in (start, entries') end))); -(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *) +(* ML pretty-printing *) val _ = PolyML.addPrettyPrinter (fn depth => fn pretty => fn set => diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Thu May 24 15:01:17 2012 +0200 +++ b/src/Pure/General/table.ML Thu May 24 15:33:45 2012 +0200 @@ -394,7 +394,7 @@ fun merge_list eq = join (fn _ => Library.merge eq); -(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *) +(* ML pretty-printing *) val _ = PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab => diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu May 24 15:01:17 2012 +0200 +++ b/src/Pure/IsaMakefile Thu May 24 15:33:45 2012 +0200 @@ -23,7 +23,7 @@ BOOTSTRAP_FILES = \ General/exn.ML \ - ML-Systems/compiler_polyml-5.3.ML \ + ML-Systems/compiler_polyml.ML \ ML-Systems/ml_name_space.ML \ ML-Systems/ml_pretty.ML \ ML-Systems/ml_system.ML \ @@ -31,7 +31,6 @@ ML-Systems/multithreading_polyml.ML \ ML-Systems/overloading_smlnj.ML \ ML-Systems/polyml.ML \ - ML-Systems/polyml_common.ML \ ML-Systems/pp_dummy.ML \ ML-Systems/proper_int.ML \ ML-Systems/single_assignment.ML \ @@ -141,10 +140,10 @@ Isar/token.ML \ Isar/toplevel.ML \ Isar/typedecl.ML \ - ML/install_pp_polyml-5.3.ML \ + ML/install_pp_polyml.ML \ ML/ml_antiquote.ML \ ML/ml_compiler.ML \ - ML/ml_compiler_polyml-5.3.ML \ + ML/ml_compiler_polyml.ML \ ML/ml_context.ML \ ML/ml_env.ML \ ML/ml_lex.ML \ diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/ML-Systems/compiler_polyml-5.3.ML --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Thu May 24 15:01:17 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ -(* Title: Pure/ML-Systems/compiler_polyml-5.3.ML - -Runtime compilation for Poly/ML 5.3.0 and 5.4.0. -*) - -local - -fun drop_newline s = - if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) - else s; - -in - -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context) - (start_line, name) verbose txt = - let - val line = Unsynchronized.ref start_line; - val in_buffer = Unsynchronized.ref (String.explode (tune_source txt)); - val out_buffer = Unsynchronized.ref ([]: string list); - fun output () = drop_newline (implode (rev (! out_buffer))); - - fun get () = - (case ! in_buffer of - [] => NONE - | c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c)); - fun put s = out_buffer := s :: ! out_buffer; - fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} = - (put (if hard then "Error: " else "Warning: "); - PolyML.prettyPrint (put, 76) msg1; - (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); - put ("At" ^ str_of_pos line name ^ "\n")); - - val parameters = - [PolyML.Compiler.CPOutStream put, - PolyML.Compiler.CPNameSpace name_space, - PolyML.Compiler.CPErrorMessageProc put_message, - PolyML.Compiler.CPLineNo (fn () => ! line), - PolyML.Compiler.CPFileName name, - PolyML.Compiler.CPPrintInAlphabeticalOrder false]; - val _ = - (while not (List.null (! in_buffer)) do - PolyML.compiler (get, parameters) ()) - handle exn => - if Exn.is_interrupt exn then reraise exn - else - (put ("Exception- " ^ General.exnMessage exn ^ " raised"); - error (output ()); reraise exn); - in if verbose then print (output ()) else () end; - -fun use_file context verbose name = - let - val instream = TextIO.openIn name; - val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); - in use_text context (1, name) verbose txt end; - -end; - diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/ML-Systems/compiler_polyml.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/compiler_polyml.ML Thu May 24 15:33:45 2012 +0200 @@ -0,0 +1,59 @@ +(* Title: Pure/ML-Systems/compiler_polyml.ML + +Runtime compilation for Poly/ML 5.3.0 or later. + +See also Pure/ML/ml_compiler_polyml.ML for advanced version. +*) + +local + +fun drop_newline s = + if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) + else s; + +in + +fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context) + (start_line, name) verbose txt = + let + val line = Unsynchronized.ref start_line; + val in_buffer = Unsynchronized.ref (String.explode (tune_source txt)); + val out_buffer = Unsynchronized.ref ([]: string list); + fun output () = drop_newline (implode (rev (! out_buffer))); + + fun get () = + (case ! in_buffer of + [] => NONE + | c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c)); + fun put s = out_buffer := s :: ! out_buffer; + fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} = + (put (if hard then "Error: " else "Warning: "); + PolyML.prettyPrint (put, 76) msg1; + (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); + put ("At" ^ str_of_pos line name ^ "\n")); + + val parameters = + [PolyML.Compiler.CPOutStream put, + PolyML.Compiler.CPNameSpace name_space, + PolyML.Compiler.CPErrorMessageProc put_message, + PolyML.Compiler.CPLineNo (fn () => ! line), + PolyML.Compiler.CPFileName name, + PolyML.Compiler.CPPrintInAlphabeticalOrder false]; + val _ = + (while not (List.null (! in_buffer)) do + PolyML.compiler (get, parameters) ()) + handle exn => + if Exn.is_interrupt exn then reraise exn + else + (put ("Exception- " ^ General.exnMessage exn ^ " raised"); + error (output ()); reraise exn); + in if verbose then print (output ()) else () end; + +fun use_file context verbose name = + let + val instream = TextIO.openIn name; + val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); + in use_text context (1, name) verbose txt end; + +end; + diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Thu May 24 15:01:17 2012 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Thu May 24 15:33:45 2012 +0200 @@ -1,16 +1,10 @@ (* Title: Pure/ML-Systems/polyml.ML + Author: Makarius -Compatibility wrapper for Poly/ML 5.3 and 5.4. +Compatibility wrapper for Poly/ML 5.3.0 or later. *) -open Thread; - -structure ML_Name_Space = -struct - open PolyML.NameSpace; - type T = PolyML.NameSpace.nameSpace; - val global = PolyML.globalNameSpace; -end; +(* exceptions *) fun reraise exn = (case PolyML.exceptionLocation exn of @@ -33,22 +27,104 @@ NONE => NONE | SOME i => if i >= 0 then NONE else SOME (~ i)); -use "ML-Systems/polyml_common.ML"; +exception Interrupt = SML90.Interrupt; + +use "General/exn.ML"; + + +(* multithreading *) + +val seconds = Time.fromReal; + +if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ()) +then () +else use "ML-Systems/single_assignment_polyml.ML"; + +open Thread; +use "ML-Systems/multithreading.ML"; use "ML-Systems/multithreading_polyml.ML"; + use "ML-Systems/unsynchronized.ML"; - val _ = PolyML.Compiler.forgetValue "ref"; val _ = PolyML.Compiler.forgetType "ref"; + +(* pervasive environment *) + +fun op before (a, _: unit) = a; + +val _ = PolyML.Compiler.forgetValue "isSome"; +val _ = PolyML.Compiler.forgetValue "getOpt"; +val _ = PolyML.Compiler.forgetValue "valOf"; +val _ = PolyML.Compiler.forgetValue "foldl"; +val _ = PolyML.Compiler.forgetValue "foldr"; +val _ = PolyML.Compiler.forgetValue "print"; +val _ = PolyML.Compiler.forgetValue "explode"; +val _ = PolyML.Compiler.forgetValue "concat"; + +val ord = SML90.ord; +val chr = SML90.chr; +val raw_explode = SML90.explode; +val implode = SML90.implode; + +fun quit () = exit 0; + + +(* ML system identification *) + +use "ML-Systems/ml_system.ML"; + + +(* ML runtime system *) + +val exception_trace = PolyML.exception_trace; +val timing = PolyML.timing; +val profiling = PolyML.profiling; + +fun profile 0 f x = f x + | profile n f x = + let + val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; + val res = Exn.capture f x; + val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; + in Exn.release res end; + val pointer_eq = PolyML.pointerEq; fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; -use "ML-Systems/compiler_polyml-5.3.ML"; + +(* ML compiler *) + +structure ML_Name_Space = +struct + open PolyML.NameSpace; + type T = PolyML.NameSpace.nameSpace; + val global = PolyML.globalNameSpace; +end; + +use "ML-Systems/use_context.ML"; +use "ML-Systems/compiler_polyml.ML"; + PolyML.Compiler.reportUnreferencedIds := true; +PolyML.Compiler.printInAlphabeticalOrder := false; +PolyML.Compiler.maxInlineSize := 80; + +fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); -(* toplevel pretty printing *) +(* ML toplevel pretty printing *) + +use "ML-Systems/ml_pretty.ML"; + +local + val depth = Unsynchronized.ref 10; +in + fun get_print_depth () = ! depth; + fun print_depth n = (depth := n; PolyML.print_depth n); +end; + +val error_depth = PolyML.error_depth; val pretty_ml = let @@ -87,5 +163,3 @@ val ml_make_string = "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))"; -use "ML-Systems/ml_system.ML"; - diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Thu May 24 15:01:17 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,88 +0,0 @@ -(* Title: Pure/ML-Systems/polyml_common.ML - -Compatibility file for Poly/ML -- common part for 5.x. -*) - -fun op before (a, _: unit) = a; - -exception Interrupt = SML90.Interrupt; - -use "General/exn.ML"; - -if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ()) -then () -else use "ML-Systems/single_assignment_polyml.ML"; - -use "ML-Systems/multithreading.ML"; -use "ML-Systems/ml_pretty.ML"; -use "ML-Systems/use_context.ML"; - -val seconds = Time.fromReal; - - - -(** ML system and platform related **) - -val _ = PolyML.Compiler.forgetValue "isSome"; -val _ = PolyML.Compiler.forgetValue "getOpt"; -val _ = PolyML.Compiler.forgetValue "valOf"; -val _ = PolyML.Compiler.forgetValue "foldl"; -val _ = PolyML.Compiler.forgetValue "foldr"; -val _ = PolyML.Compiler.forgetValue "print"; -val _ = PolyML.Compiler.forgetValue "explode"; -val _ = PolyML.Compiler.forgetValue "concat"; - - -(* Compiler options *) - -PolyML.Compiler.printInAlphabeticalOrder := false; -PolyML.Compiler.maxInlineSize := 80; - - -(* old Poly/ML emulation *) - -fun quit () = exit 0; - - -(* restore old-style character / string functions *) - -val ord = SML90.ord; -val chr = SML90.chr; -val raw_explode = SML90.explode; -val implode = SML90.implode; - - -(* prompts *) - -fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); - - -(* toplevel printing *) - -local - val depth = ref 10; -in - fun get_print_depth () = ! depth; - fun print_depth n = (depth := n; PolyML.print_depth n); -end; - -val error_depth = PolyML.error_depth; - -val ml_make_string = "PolyML.makestring"; - - - -(** Runtime system **) - -val exception_trace = PolyML.exception_trace; -val timing = PolyML.timing; -val profiling = PolyML.profiling; - -fun profile 0 f x = f x - | profile n f x = - let - val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; - val res = Exn.capture f x; - val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; - in Exn.release res end; - diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/ML/install_pp_polyml-5.3.ML --- a/src/Pure/ML/install_pp_polyml-5.3.ML Thu May 24 15:01:17 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ -(* Title: Pure/ML/install_pp_polyml-5.3.ML - Author: Makarius - -Extra toplevel pretty-printing for Poly/ML 5.3.0. -*) - -PolyML.addPrettyPrinter (fn depth => fn _ => fn str => - ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str))); - -PolyML.addPrettyPrinter (fn depth => fn _ => fn tree => - ml_pretty (Pretty.to_ML (XML.pretty depth tree))); - -PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => - pretty (Synchronized.value var, depth)); - -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => - (case Future.peek x of - NONE => PolyML.PrettyString "" - | SOME (Exn.Exn _) => PolyML.PrettyString "" - | SOME (Exn.Res y) => pretty (y, depth))); - -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => - (case Lazy.peek x of - NONE => PolyML.PrettyString "" - | SOME (Exn.Exn _) => PolyML.PrettyString "" - | SOME (Exn.Res y) => pretty (y, depth))); - -PolyML.addPrettyPrinter (fn depth => fn _ => fn tm => - let - open PolyML; - val from_ML = Pretty.from_ML o pretty_ml; - fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; - fun prt_apps name = Pretty.enum "," (name ^ " (") ")"; - fun prt_term parens dp (t as _ $ _) = - op :: (strip_comb t) - |> map_index (fn (i, u) => prt_term true (dp - i - 1) u) - |> Pretty.separate " $" - |> (if parens then Pretty.enclose "(" ")" else Pretty.block) - | prt_term _ dp (Abs (x, T, body)) = - prt_apps "Abs" - [from_ML (prettyRepresentation (x, dp - 1)), - from_ML (prettyRepresentation (T, dp - 2)), - prt_term false (dp - 3) body] - | prt_term _ dp (Const const) = - prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1))) - | prt_term _ dp (Free free) = - prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1))) - | prt_term _ dp (Var var) = - prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1))) - | prt_term _ dp (Bound i) = - prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1))); - in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end); - diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/ML/install_pp_polyml.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/install_pp_polyml.ML Thu May 24 15:33:45 2012 +0200 @@ -0,0 +1,53 @@ +(* Title: Pure/ML/install_pp_polyml.ML + Author: Makarius + +Extra toplevel pretty-printing for Poly/ML 5.3.0 or later. +*) + +PolyML.addPrettyPrinter (fn depth => fn _ => fn str => + ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str))); + +PolyML.addPrettyPrinter (fn depth => fn _ => fn tree => + ml_pretty (Pretty.to_ML (XML.pretty depth tree))); + +PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => + pretty (Synchronized.value var, depth)); + +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => + (case Future.peek x of + NONE => PolyML.PrettyString "" + | SOME (Exn.Exn _) => PolyML.PrettyString "" + | SOME (Exn.Res y) => pretty (y, depth))); + +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => + (case Lazy.peek x of + NONE => PolyML.PrettyString "" + | SOME (Exn.Exn _) => PolyML.PrettyString "" + | SOME (Exn.Res y) => pretty (y, depth))); + +PolyML.addPrettyPrinter (fn depth => fn _ => fn tm => + let + open PolyML; + val from_ML = Pretty.from_ML o pretty_ml; + fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; + fun prt_apps name = Pretty.enum "," (name ^ " (") ")"; + fun prt_term parens dp (t as _ $ _) = + op :: (strip_comb t) + |> map_index (fn (i, u) => prt_term true (dp - i - 1) u) + |> Pretty.separate " $" + |> (if parens then Pretty.enclose "(" ")" else Pretty.block) + | prt_term _ dp (Abs (x, T, body)) = + prt_apps "Abs" + [from_ML (prettyRepresentation (x, dp - 1)), + from_ML (prettyRepresentation (T, dp - 2)), + prt_term false (dp - 3) body] + | prt_term _ dp (Const const) = + prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1))) + | prt_term _ dp (Free free) = + prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1))) + | prt_term _ dp (Var var) = + prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1))) + | prt_term _ dp (Bound i) = + prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1))); + in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end); + diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu May 24 15:01:17 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,202 +0,0 @@ -(* Title: Pure/ML/ml_compiler_polyml-5.3.ML - Author: Makarius - -Advanced runtime compilation for Poly/ML 5.3.0 or later. -*) - -structure ML_Compiler: ML_COMPILER = -struct - -(* source locations *) - -fun position_of (loc: PolyML.location) = - let - val {file = text, startLine = line, startPosition = offset, - endLine = _, endPosition = end_offset} = loc; - val props = - (case YXML.parse text of - XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else [] - | XML.Text s => Position.file_name s); - in - Position.make {line = line, offset = offset, end_offset = end_offset, props = props} - end; - -fun exn_position exn = - (case PolyML.exceptionLocation exn of - NONE => Position.none - | SOME loc => position_of loc); - -val exn_messages = Runtime.exn_messages exn_position; -val exn_message = Runtime.exn_message exn_position; - - -(* parse trees *) - -fun report_parse_tree depth space = - let - val reported_text = - (case Context.thread_data () of - SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt - | _ => Position.reported_text); - - fun reported_entity kind loc decl = - reported_text (position_of loc) - (Isabelle_Markup.entityN, - (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) ""; - - fun reported loc (PolyML.PTtype types) = - cons - (PolyML.NameSpace.displayTypeExpression (types, depth, space) - |> pretty_ml |> Pretty.from_ML |> Pretty.string_of - |> reported_text (position_of loc) Isabelle_Markup.ML_typing) - | reported loc (PolyML.PTdeclaredAt decl) = - cons (reported_entity Isabelle_Markup.ML_defN loc decl) - | reported loc (PolyML.PTopenedAt decl) = - cons (reported_entity Isabelle_Markup.ML_openN loc decl) - | reported loc (PolyML.PTstructureAt decl) = - cons (reported_entity Isabelle_Markup.ML_structN loc decl) - | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) - | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) - | reported _ _ = I - and reported_tree (loc, props) = fold (reported loc) props; - in fn tree => Output.report (implode (reported_tree tree [])) end; - - -(* eval ML source tokens *) - -fun eval verbose pos toks = - let - val _ = Secure.secure_mltext (); - val space = ML_Env.name_space; - - - (* input *) - - val location_props = - op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties - (filter (member (op =) - [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos)))); - - val input_buffer = - Unsynchronized.ref (toks |> map - (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of))); - - fun get () = - (case ! input_buffer of - (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c) - | ([], _) :: rest => (input_buffer := rest; SOME #" ") - | [] => NONE); - - fun get_pos () = - (case ! input_buffer of - (_ :: _, tok) :: _ => ML_Lex.pos_of tok - | ([], tok) :: _ => ML_Lex.end_pos_of tok - | [] => Position.none); - - - (* output channels *) - - val writeln_buffer = Unsynchronized.ref Buffer.empty; - fun write s = Unsynchronized.change writeln_buffer (Buffer.add s); - fun output_writeln () = writeln (Buffer.content (! writeln_buffer)); - - val warnings = Unsynchronized.ref ([]: string list); - fun warn msg = Unsynchronized.change warnings (cons msg); - fun output_warnings () = List.app warning (rev (! warnings)); - - val error_buffer = Unsynchronized.ref Buffer.empty; - fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n"); - fun flush_error () = writeln (Buffer.content (! error_buffer)); - fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer))); - - fun message {message = msg, hard, location = loc, context = _} = - let - val pos = position_of loc; - val txt = - (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report) - ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^ - Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^ - Position.reported_text pos Isabelle_Markup.report ""; - in if hard then err txt else warn txt end; - - - (* results *) - - val depth = get_print_depth (); - - fun apply_result {fixes, types, signatures, structures, functors, values} = - let - fun display disp x = - if depth > 0 then - (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n") - else (); - - fun apply_fix (a, b) = - (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b)); - fun apply_type (a, b) = - (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space)); - fun apply_sig (a, b) = - (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space)); - fun apply_struct (a, b) = - (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space)); - fun apply_funct (a, b) = - (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space)); - fun apply_val (a, b) = - (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space)); - 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; - - exception STATIC_ERRORS of unit; - - fun result_fun (phase1, phase2) () = - ((case phase1 of - NONE => () - | SOME parse_tree => report_parse_tree depth space parse_tree); - (case phase2 of - NONE => raise STATIC_ERRORS () - | SOME code => - apply_result - ((code - |> Runtime.debugging - |> Runtime.toplevel_error (err o exn_message)) ()))); - - - (* compiler invocation *) - - val parameters = - [PolyML.Compiler.CPOutStream write, - PolyML.Compiler.CPNameSpace space, - PolyML.Compiler.CPErrorMessageProc message, - PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos), - PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), - PolyML.Compiler.CPFileName location_props, - PolyML.Compiler.CPCompilerResultFun result_fun, - PolyML.Compiler.CPPrintInAlphabeticalOrder false]; - val _ = - (while not (List.null (! input_buffer)) do - PolyML.compiler (get, parameters) ()) - handle exn => - if Exn.is_interrupt exn then reraise exn - else - let - val exn_msg = - (case exn of - STATIC_ERRORS () => "" - | Runtime.TOPLEVEL_ERROR => "" - | _ => "Exception- " ^ General.exnMessage exn ^ " raised"); - val _ = output_warnings (); - val _ = output_writeln (); - in raise_error exn_msg end; - in - if verbose then (output_warnings (); flush_error (); output_writeln ()) - else () - end; - -end; - diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/ML/ml_compiler_polyml.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_compiler_polyml.ML Thu May 24 15:33:45 2012 +0200 @@ -0,0 +1,202 @@ +(* Title: Pure/ML/ml_compiler_polyml.ML + Author: Makarius + +Advanced runtime compilation for Poly/ML 5.3.0 or later. +*) + +structure ML_Compiler: ML_COMPILER = +struct + +(* source locations *) + +fun position_of (loc: PolyML.location) = + let + val {file = text, startLine = line, startPosition = offset, + endLine = _, endPosition = end_offset} = loc; + val props = + (case YXML.parse text of + XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else [] + | XML.Text s => Position.file_name s); + in + Position.make {line = line, offset = offset, end_offset = end_offset, props = props} + end; + +fun exn_position exn = + (case PolyML.exceptionLocation exn of + NONE => Position.none + | SOME loc => position_of loc); + +val exn_messages = Runtime.exn_messages exn_position; +val exn_message = Runtime.exn_message exn_position; + + +(* parse trees *) + +fun report_parse_tree depth space = + let + val reported_text = + (case Context.thread_data () of + SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt + | _ => Position.reported_text); + + fun reported_entity kind loc decl = + reported_text (position_of loc) + (Isabelle_Markup.entityN, + (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) ""; + + fun reported loc (PolyML.PTtype types) = + cons + (PolyML.NameSpace.displayTypeExpression (types, depth, space) + |> pretty_ml |> Pretty.from_ML |> Pretty.string_of + |> reported_text (position_of loc) Isabelle_Markup.ML_typing) + | reported loc (PolyML.PTdeclaredAt decl) = + cons (reported_entity Isabelle_Markup.ML_defN loc decl) + | reported loc (PolyML.PTopenedAt decl) = + cons (reported_entity Isabelle_Markup.ML_openN loc decl) + | reported loc (PolyML.PTstructureAt decl) = + cons (reported_entity Isabelle_Markup.ML_structN loc decl) + | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) + | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) + | reported _ _ = I + and reported_tree (loc, props) = fold (reported loc) props; + in fn tree => Output.report (implode (reported_tree tree [])) end; + + +(* eval ML source tokens *) + +fun eval verbose pos toks = + let + val _ = Secure.secure_mltext (); + val space = ML_Env.name_space; + + + (* input *) + + val location_props = + op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties + (filter (member (op =) + [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos)))); + + val input_buffer = + Unsynchronized.ref (toks |> map + (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of))); + + fun get () = + (case ! input_buffer of + (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c) + | ([], _) :: rest => (input_buffer := rest; SOME #" ") + | [] => NONE); + + fun get_pos () = + (case ! input_buffer of + (_ :: _, tok) :: _ => ML_Lex.pos_of tok + | ([], tok) :: _ => ML_Lex.end_pos_of tok + | [] => Position.none); + + + (* output channels *) + + val writeln_buffer = Unsynchronized.ref Buffer.empty; + fun write s = Unsynchronized.change writeln_buffer (Buffer.add s); + fun output_writeln () = writeln (Buffer.content (! writeln_buffer)); + + val warnings = Unsynchronized.ref ([]: string list); + fun warn msg = Unsynchronized.change warnings (cons msg); + fun output_warnings () = List.app warning (rev (! warnings)); + + val error_buffer = Unsynchronized.ref Buffer.empty; + fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n"); + fun flush_error () = writeln (Buffer.content (! error_buffer)); + fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer))); + + fun message {message = msg, hard, location = loc, context = _} = + let + val pos = position_of loc; + val txt = + (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report) + ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^ + Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^ + Position.reported_text pos Isabelle_Markup.report ""; + in if hard then err txt else warn txt end; + + + (* results *) + + val depth = get_print_depth (); + + fun apply_result {fixes, types, signatures, structures, functors, values} = + let + fun display disp x = + if depth > 0 then + (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n") + else (); + + fun apply_fix (a, b) = + (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b)); + fun apply_type (a, b) = + (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space)); + fun apply_sig (a, b) = + (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space)); + fun apply_struct (a, b) = + (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space)); + fun apply_funct (a, b) = + (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space)); + fun apply_val (a, b) = + (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space)); + 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; + + exception STATIC_ERRORS of unit; + + fun result_fun (phase1, phase2) () = + ((case phase1 of + NONE => () + | SOME parse_tree => report_parse_tree depth space parse_tree); + (case phase2 of + NONE => raise STATIC_ERRORS () + | SOME code => + apply_result + ((code + |> Runtime.debugging + |> Runtime.toplevel_error (err o exn_message)) ()))); + + + (* compiler invocation *) + + val parameters = + [PolyML.Compiler.CPOutStream write, + PolyML.Compiler.CPNameSpace space, + PolyML.Compiler.CPErrorMessageProc message, + PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos), + PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), + PolyML.Compiler.CPFileName location_props, + PolyML.Compiler.CPCompilerResultFun result_fun, + PolyML.Compiler.CPPrintInAlphabeticalOrder false]; + val _ = + (while not (List.null (! input_buffer)) do + PolyML.compiler (get, parameters) ()) + handle exn => + if Exn.is_interrupt exn then reraise exn + else + let + val exn_msg = + (case exn of + STATIC_ERRORS () => "" + | Runtime.TOPLEVEL_ERROR => "" + | _ => "Exception- " ^ General.exnMessage exn ^ " raised"); + val _ = output_warnings (); + val _ = output_writeln (); + in raise_error exn_msg end; + in + if verbose then (output_warnings (); flush_error (); output_writeln ()) + else () + end; + +end; + diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu May 24 15:01:17 2012 +0200 +++ b/src/Pure/ROOT.ML Thu May 24 15:33:45 2012 +0200 @@ -74,7 +74,7 @@ if Multithreading.available then () else use "Concurrent/single_assignment_sequential.ML"; -if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML"; +if ML_System.is_polyml then use "Concurrent/time_limit.ML" else (); if Multithreading.available then use "Concurrent/bash.ML" @@ -191,8 +191,7 @@ use "ML/ml_env.ML"; use "Isar/runtime.ML"; use "ML/ml_compiler.ML"; -if ML_System.is_smlnj then () -else use "ML/ml_compiler_polyml-5.3.ML"; +if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else (); use "ML/ml_context.ML"; (*theory sources*) diff -r 59ec72d3d0b9 -r c81801f881b3 src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Thu May 24 15:01:17 2012 +0200 +++ b/src/Pure/pure_setup.ML Thu May 24 15:33:45 2012 +0200 @@ -36,9 +36,7 @@ toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"\")"; toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; -if ML_System.is_polyml -then use "ML/install_pp_polyml-5.3.ML" -else (); +if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else (); (* ML toplevel use commands *)