do not open Legacy by default;
authorwenzelm
Tue May 18 00:01:03 2010 +0200 (2010-05-18)
changeset 369617b14afc02fc4
parent 36960 01594f816e3a
child 36972 aa4bc5a4be1d
do not open Legacy by default;
NEWS
src/Pure/ROOT.ML
     1.1 --- a/NEWS	Mon May 17 23:54:15 2010 +0200
     1.2 +++ b/NEWS	Tue May 18 00:01:03 2010 +0200
     1.3 @@ -502,8 +502,8 @@
     1.4  context actually works, but under normal circumstances one needs to
     1.5  pass the proper local context through the code!
     1.6  
     1.7 -* Renamed some important ML structures, while keeping the old names as
     1.8 -legacy aliases for some time:
     1.9 +* Renamed some important ML structures, while keeping the old names
    1.10 +for some time as aliases within the structure Legacy:
    1.11  
    1.12    OuterKeyword  ~>  Keyword
    1.13    OuterLex      ~>  Token
    1.14 @@ -511,6 +511,9 @@
    1.15    OuterSyntax   ~>  Outer_Syntax
    1.16    SpecParse     ~>  Parse_Spec
    1.17  
    1.18 +Note that "open Legacy" simplifies porting of sources, but forgetting
    1.19 +to remove it again will complicate porting again in the future.
    1.20 +
    1.21  
    1.22  *** System ***
    1.23  
     2.1 --- a/src/Pure/ROOT.ML	Mon May 17 23:54:15 2010 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Tue May 18 00:01:03 2010 +0200
     2.3 @@ -312,4 +312,3 @@
     2.4  
     2.5  end;
     2.6  
     2.7 -open Legacy;  (* FIXME *)