# HG changeset patch # User wenzelm # Date 1013445058 -3600 # Node ID 368966ceafe5ad86b1235bdb6e3ff7aac447cfa3 # Parent d7f8dfaad46d61a8dcb2ae4e30bc458958bd358a ML-Systems/smlnj-compiler.ML compatibility tweak; diff -r d7f8dfaad46d -r 368966ceafe5 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Feb 11 10:56:33 2002 +0100 +++ b/src/Pure/IsaMakefile Mon Feb 11 17:30:58 2002 +0100 @@ -40,20 +40,20 @@ Isar/rule_cases.ML Isar/session.ML Isar/skip_proof.ML \ Isar/thy_header.ML Isar/toplevel.ML ML-Systems/mlworks.ML \ ML-Systems/polyml-3.x.ML ML-Systems/polyml.ML \ - ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML Proof/ROOT.ML \ - Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ - Proof/proofchecker.ML Proof/reconstruct.ML ROOT.ML Syntax/ROOT.ML \ - Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ - Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \ - Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \ - Thy/ROOT.ML Thy/html.ML Thy/latex.ML Thy/present.ML \ - Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_info.ML Thy/thy_load.ML \ - Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML \ - codegen.ML context.ML display.ML drule.ML envir.ML goals.ML \ - install_pp.ML library.ML logic.ML meta_simplifier.ML net.ML \ - pattern.ML proof_general.ML proofterm.ML pure.ML pure_thy.ML search.ML sign.ML \ - sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML \ - thm.ML type.ML type_infer.ML unify.ML + ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-0.93.ML \ + ML-Systems/smlnj.ML Proof/ROOT.ML Proof/proof_rewrite_rules.ML \ + Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ + ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \ + Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML \ + Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML \ + Syntax/type_ext.ML Thy/ROOT.ML Thy/html.ML Thy/latex.ML \ + Thy/present.ML Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_info.ML \ + Thy/thy_load.ML Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML \ + axclass.ML basis.ML codegen.ML context.ML display.ML drule.ML \ + envir.ML goals.ML install_pp.ML library.ML logic.ML \ + meta_simplifier.ML net.ML pattern.ML proof_general.ML proofterm.ML \ + pure.ML pure_thy.ML search.ML sign.ML sorts.ML tactic.ML tctical.ML \ + term.ML theory.ML theory_data.ML thm.ML type.ML type_infer.ML unify.ML @./mk diff -r d7f8dfaad46d -r 368966ceafe5 src/Pure/ML-Systems/smlnj-compiler.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/smlnj-compiler.ML Mon Feb 11 17:30:58 2002 +0100 @@ -0,0 +1,15 @@ +(* Title: Pure/ML-Systems/smlnj.ML + ID: $Id$ + Author: Markus Wenzel, LMU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Compatibility tweak for later versions of Standard ML of New Jersey 110. +*) + +structure Compiler = +struct + structure Control = Control; + structure PrettyPrint = PrettyPrint; + structure PPTable = CompilerPPTable; + structure Interact = Backend.Interact; +end; diff -r d7f8dfaad46d -r 368966ceafe5 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Mon Feb 11 10:56:33 2002 +0100 +++ b/src/Pure/ML-Systems/smlnj.ML Mon Feb 11 17:30:58 2002 +0100 @@ -1,10 +1,16 @@ (* Title: Pure/ML-Systems/smlnj.ML ID: $Id$ Author: Carsten Clasohm and Markus Wenzel, TU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) Compatibility file for Standard ML of New Jersey 110 or later. *) +(case #version_id (Compiler.version) of + [110, x] => if x >= 35 then use "ML-Systems/smlnj-compiler.ML" else () +| _ => ()); + + (** ML system related **) (* restore old-style character / string functions *)