# HG changeset patch # User wenzelm # Date 1281526776 -7200 # Node ID d6afb77b0f6daee82c1451a49e2bce0fa0a95d50 # Parent 01d2ef471ffe979e741f5f35a0183e0f3eb98088 more precise and more maintainable dependencies; diff -r 01d2ef471ffe -r d6afb77b0f6d src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Aug 11 12:50:33 2010 +0200 +++ b/src/Pure/IsaMakefile Wed Aug 11 13:39:36 2010 +0200 @@ -19,19 +19,33 @@ ## Pure -BOOTSTRAP_FILES = ML-Systems/bash.ML ML-Systems/compiler_polyml-5.0.ML \ - ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML \ - ML-Systems/ml_name_space.ML ML-Systems/ml_pretty.ML \ - ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \ - ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \ - ML-Systems/polyml-5.1.ML ML-Systems/polyml-5.2.ML \ - ML-Systems/polyml-5.2.1.ML ML-Systems/polyml.ML \ - ML-Systems/polyml_common.ML ML-Systems/pp_polyml.ML \ - ML-Systems/proper_int.ML ML-Systems/single_assignment.ML \ - ML-Systems/single_assignment_polyml.ML ML-Systems/smlnj.ML \ - ML-Systems/thread_dummy.ML ML-Systems/timing.ML \ - ML-Systems/time_limit.ML ML-Systems/universal.ML \ - ML-Systems/unsynchronized.ML +BOOTSTRAP_FILES = \ + ML-Systems/bash.ML \ + ML-Systems/compiler_polyml-5.0.ML \ + ML-Systems/compiler_polyml-5.2.ML \ + ML-Systems/compiler_polyml-5.3.ML \ + ML-Systems/ml_name_space.ML \ + ML-Systems/ml_pretty.ML \ + ML-Systems/multithreading.ML \ + ML-Systems/multithreading_polyml.ML \ + ML-Systems/overloading_smlnj.ML \ + ML-Systems/polyml-5.0.ML \ + ML-Systems/polyml-5.1.ML \ + ML-Systems/polyml-5.2.1.ML \ + ML-Systems/polyml-5.2.ML \ + ML-Systems/polyml.ML \ + ML-Systems/polyml_common.ML \ + ML-Systems/pp_polyml.ML \ + ML-Systems/proper_int.ML \ + ML-Systems/single_assignment.ML \ + ML-Systems/single_assignment_polyml.ML \ + ML-Systems/smlnj.ML \ + ML-Systems/thread_dummy.ML \ + ML-Systems/time_limit.ML \ + ML-Systems/timing.ML \ + ML-Systems/universal.ML \ + ML-Systems/unsynchronized.ML \ + ML-Systems/use_context.ML RAW: $(OUT)/RAW @@ -41,92 +55,205 @@ Pure: $(OUT)/Pure -$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/cache.ML \ - Concurrent/future.ML Concurrent/lazy.ML \ - Concurrent/lazy_sequential.ML Concurrent/mailbox.ML \ - Concurrent/par_list.ML Concurrent/par_list_sequential.ML \ - Concurrent/simple_thread.ML Concurrent/single_assignment.ML \ - Concurrent/single_assignment_sequential.ML \ - Concurrent/synchronized.ML Concurrent/synchronized_sequential.ML \ - Concurrent/task_queue.ML General/alist.ML General/antiquote.ML \ - General/balanced_tree.ML General/basics.ML General/binding.ML \ - General/buffer.ML General/exn.ML General/file.ML General/graph.ML \ - General/heap.ML General/integer.ML General/long_name.ML \ - General/markup.ML General/name_space.ML General/ord_list.ML \ - General/output.ML General/path.ML General/position.ML \ - General/pretty.ML General/print_mode.ML General/properties.ML \ - General/queue.ML General/same.ML General/scan.ML General/sha1.ML \ - General/sha1_polyml.ML General/secure.ML General/seq.ML \ - General/source.ML General/stack.ML General/symbol.ML \ - General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \ - General/xml_data.ML General/yxml.ML Isar/args.ML Isar/attrib.ML \ - Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \ - Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \ - Isar/context_rules.ML Isar/element.ML Isar/expression.ML \ - Isar/generic_target.ML Isar/isar_cmd.ML Isar/isar_document.ML \ - Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML \ - Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \ - Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \ - Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML \ - Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML \ - Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \ - Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \ - Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML \ - Isar/theory_target.ML Isar/token.ML Isar/toplevel.ML \ - Isar/typedecl.ML ML/ml_antiquote.ML ML/ml_compiler.ML \ - ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \ - ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \ - ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML \ - ML-Systems/use_context.ML Proof/extraction.ML PIDE/document.ML \ - Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ - Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML \ - ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \ - ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \ - ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \ - ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML \ - ProofGeneral/proof_general_emacs.ML General/yxml.ML Isar/args.ML \ - Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \ - Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \ - Isar/context_rules.ML Isar/element.ML Isar/expression.ML \ - Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML \ - Isar/keyword.ML Isar/local_defs.ML Isar/local_syntax.ML \ - Isar/local_theory.ML Isar/locale.ML Isar/method.ML \ - Isar/object_logic.ML Isar/obtain.ML Isar/outer_syntax.ML \ - Isar/overloading.ML Isar/parse.ML Isar/parse_spec.ML \ - Isar/parse_value.ML Isar/proof.ML Isar/proof_context.ML \ - Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \ - Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML \ - Isar/spec_rules.ML Isar/specification.ML Isar/theory_target.ML \ - Isar/token.ML Isar/toplevel.ML Isar/typedecl.ML ML/ml_antiquote.ML \ - ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \ - ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \ - ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \ - ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \ - Proof/extraction.ML PIDE/document.ML Proof/proof_rewrite_rules.ML \ - Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ - ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \ - ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \ - ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \ - ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \ - ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \ - ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \ - Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ - Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \ - Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML \ - System/isabelle_process.ML System/isar.ML System/session.ML \ - Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML \ - Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \ - Thy/thy_output.ML Thy/thy_syntax.ML Tools/find_consts.ML \ - Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML \ - assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \ - consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \ - drule.ML envir.ML facts.ML goal.ML goal_display.ML interpretation.ML \ - item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \ - morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML \ - primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \ - sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tactical.ML \ - term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML \ - type_infer.ML unify.ML variable.ML +$(OUT)/Pure: $(BOOTSTRAP_FILES) \ + Concurrent/cache.ML \ + Concurrent/future.ML \ + Concurrent/lazy.ML \ + Concurrent/lazy_sequential.ML \ + Concurrent/mailbox.ML \ + Concurrent/par_list.ML \ + Concurrent/par_list_sequential.ML \ + Concurrent/simple_thread.ML \ + Concurrent/single_assignment.ML \ + Concurrent/single_assignment_sequential.ML \ + Concurrent/synchronized.ML \ + Concurrent/synchronized_sequential.ML \ + Concurrent/task_queue.ML \ + General/alist.ML \ + General/antiquote.ML \ + General/balanced_tree.ML \ + General/basics.ML \ + General/binding.ML \ + General/buffer.ML \ + General/exn.ML \ + General/file.ML \ + General/graph.ML \ + General/heap.ML \ + General/integer.ML \ + General/long_name.ML \ + General/markup.ML \ + General/name_space.ML \ + General/ord_list.ML \ + General/output.ML \ + General/path.ML \ + General/position.ML \ + General/pretty.ML \ + General/print_mode.ML \ + General/properties.ML \ + General/queue.ML \ + General/same.ML \ + General/scan.ML \ + General/secure.ML \ + General/seq.ML \ + General/sha1.ML \ + General/sha1_polyml.ML \ + General/source.ML \ + General/stack.ML \ + General/symbol.ML \ + General/symbol_pos.ML \ + General/table.ML \ + General/url.ML \ + General/xml.ML \ + General/xml_data.ML \ + General/yxml.ML \ + Isar/args.ML \ + Isar/attrib.ML \ + Isar/auto_bind.ML \ + Isar/calculation.ML \ + Isar/class.ML \ + Isar/class_target.ML \ + Isar/code.ML \ + Isar/constdefs.ML \ + Isar/context_rules.ML \ + Isar/element.ML \ + Isar/expression.ML \ + Isar/generic_target.ML \ + Isar/isar_cmd.ML \ + Isar/isar_document.ML \ + Isar/isar_syn.ML \ + Isar/keyword.ML \ + Isar/local_defs.ML \ + Isar/local_syntax.ML \ + Isar/local_theory.ML \ + Isar/locale.ML \ + Isar/method.ML \ + Isar/object_logic.ML \ + Isar/obtain.ML \ + Isar/outer_syntax.ML \ + Isar/overloading.ML \ + Isar/parse.ML \ + Isar/parse_spec.ML \ + Isar/parse_value.ML \ + Isar/proof.ML \ + Isar/proof_context.ML \ + Isar/proof_display.ML \ + Isar/proof_node.ML \ + Isar/rule_cases.ML \ + Isar/rule_insts.ML \ + Isar/runtime.ML \ + Isar/skip_proof.ML \ + Isar/spec_rules.ML \ + Isar/specification.ML \ + Isar/theory_target.ML \ + 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_context.ML \ + ML/ml_env.ML \ + ML/ml_lex.ML \ + ML/ml_parse.ML \ + ML/ml_syntax.ML \ + ML/ml_thms.ML \ + PIDE/document.ML \ + Proof/extraction.ML \ + Proof/proof_rewrite_rules.ML \ + Proof/proof_syntax.ML \ + Proof/proofchecker.ML \ + Proof/reconstruct.ML \ + ProofGeneral/pgip.ML \ + ProofGeneral/pgip_input.ML \ + ProofGeneral/pgip_isabelle.ML \ + ProofGeneral/pgip_markup.ML \ + ProofGeneral/pgip_output.ML \ + ProofGeneral/pgip_parser.ML \ + ProofGeneral/pgip_tests.ML \ + ProofGeneral/pgip_types.ML \ + ProofGeneral/pgml.ML \ + ProofGeneral/preferences.ML \ + ProofGeneral/proof_general_emacs.ML \ + ProofGeneral/proof_general_pgip.ML \ + Pure.thy \ + ROOT.ML \ + Syntax/ast.ML \ + Syntax/lexicon.ML \ + Syntax/mixfix.ML \ + Syntax/parser.ML \ + Syntax/printer.ML \ + Syntax/simple_syntax.ML \ + Syntax/syn_ext.ML \ + Syntax/syn_trans.ML \ + Syntax/syntax.ML \ + Syntax/type_ext.ML \ + System/isabelle_process.ML \ + System/isar.ML \ + System/session.ML \ + Thy/html.ML \ + Thy/latex.ML \ + Thy/present.ML \ + Thy/term_style.ML \ + Thy/thm_deps.ML \ + Thy/thy_header.ML \ + Thy/thy_info.ML \ + Thy/thy_load.ML \ + Thy/thy_output.ML \ + Thy/thy_syntax.ML \ + Tools/find_consts.ML \ + Tools/find_theorems.ML \ + Tools/named_thms.ML \ + Tools/xml_syntax.ML \ + assumption.ML \ + axclass.ML \ + codegen.ML \ + config.ML \ + conjunction.ML \ + consts.ML \ + context.ML \ + context_position.ML \ + conv.ML \ + defs.ML \ + display.ML \ + drule.ML \ + envir.ML \ + facts.ML \ + goal.ML \ + goal_display.ML \ + interpretation.ML \ + item_net.ML \ + library.ML \ + logic.ML \ + meta_simplifier.ML \ + more_thm.ML \ + morphism.ML \ + name.ML \ + net.ML \ + old_goals.ML \ + old_term.ML \ + pattern.ML \ + primitive_defs.ML \ + proofterm.ML \ + pure_setup.ML \ + pure_thy.ML \ + search.ML \ + sign.ML \ + simplifier.ML \ + sorts.ML \ + subgoal.ML \ + tactic.ML \ + tactical.ML \ + term.ML \ + term_ord.ML \ + term_subst.ML \ + theory.ML \ + thm.ML \ + type.ML \ + type_infer.ML \ + unify.ML \ + variable.ML @./mk @@ -141,5 +268,4 @@ ## clean clean: - @rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz \ - $(LOG)/Pure-ProofGeneral.gz + @rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz $(LOG)/Pure-ProofGeneral.gz diff -r 01d2ef471ffe -r d6afb77b0f6d src/Pure/ML-Systems/install_pp_polyml-5.3.ML --- a/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Wed Aug 11 12:50:33 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,46 +0,0 @@ -(* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML - -Extra toplevel pretty-printing for Poly/ML 5.3.0. -*) - -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.Result 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.Result 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 01d2ef471ffe -r d6afb77b0f6d src/Pure/ML-Systems/install_pp_polyml.ML --- a/src/Pure/ML-Systems/install_pp_polyml.ML Wed Aug 11 12:50:33 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -(* Title: Pure/ML-Systems/install_pp_polyml.ML - -Extra toplevel pretty-printing for Poly/ML. -*) - -PolyML.install_pp - (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) => - (case Future.peek x of - NONE => str "" - | SOME (Exn.Exn _) => str "" - | SOME (Exn.Result y) => print (y, depth))); - -PolyML.install_pp - (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) => - (case Lazy.peek x of - NONE => str "" - | SOME (Exn.Exn _) => str "" - | SOME (Exn.Result y) => print (y, depth))); - diff -r 01d2ef471ffe -r d6afb77b0f6d src/Pure/ML/install_pp_polyml-5.3.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/install_pp_polyml-5.3.ML Wed Aug 11 13:39:36 2010 +0200 @@ -0,0 +1,47 @@ +(* 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 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.Result 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.Result 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 01d2ef471ffe -r d6afb77b0f6d 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 Wed Aug 11 13:39:36 2010 +0200 @@ -0,0 +1,20 @@ +(* Title: Pure/ML/install_pp_polyml.ML + Author: Makarius + +Extra toplevel pretty-printing for Poly/ML. +*) + +PolyML.install_pp + (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) => + (case Future.peek x of + NONE => str "" + | SOME (Exn.Exn _) => str "" + | SOME (Exn.Result y) => print (y, depth))); + +PolyML.install_pp + (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) => + (case Lazy.peek x of + NONE => str "" + | SOME (Exn.Exn _) => str "" + | SOME (Exn.Result y) => print (y, depth))); + diff -r 01d2ef471ffe -r d6afb77b0f6d src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Wed Aug 11 12:50:33 2010 +0200 +++ b/src/Pure/pure_setup.ML Wed Aug 11 13:39:36 2010 +0200 @@ -40,9 +40,9 @@ toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; if ml_system = "polyml-5.3.0" -then use "ML-Systems/install_pp_polyml-5.3.ML" +then use "ML/install_pp_polyml-5.3.ML" else if String.isPrefix "polyml" ml_system -then use "ML-Systems/install_pp_polyml.ML" +then use "ML/install_pp_polyml.ML" else (); if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then