removed token_trans.ML (some content moved to syn_ext.ML);
authorwenzelm
Sat Apr 23 19:51:24 2005 +0200 (2005-04-23)
changeset 1583378109c7012ed
parent 15832 df958c7afe50
child 15834 a5166d054683
removed token_trans.ML (some content moved to syn_ext.ML);
src/Pure/Syntax/ROOT.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/type_ext.ML
     1.1 --- a/src/Pure/Syntax/ROOT.ML	Sat Apr 23 19:51:11 2005 +0200
     1.2 +++ b/src/Pure/Syntax/ROOT.ML	Sat Apr 23 19:51:24 2005 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  *)
     1.5  
     1.6  use "lexicon.ML";
     1.7 -use "token_trans.ML";
     1.8  use "ast.ML";
     1.9  use "syn_ext.ML";
    1.10  use "parser.ML";
    1.11 @@ -18,7 +17,6 @@
    1.12  
    1.13  (*hiding private stuff*)
    1.14  structure Lexicon = Hidden;
    1.15 -structure TokenTrans = Hidden;
    1.16  structure Ast = Hidden;
    1.17  structure SynExt = Hidden;
    1.18  structure Parser = Hidden;
     2.1 --- a/src/Pure/Syntax/syntax.ML	Sat Apr 23 19:51:11 2005 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Apr 23 19:51:24 2005 +0200
     2.3 @@ -15,7 +15,6 @@
     2.4  
     2.5  signature SYNTAX =
     2.6  sig
     2.7 -  include TOKEN_TRANS0
     2.8    include AST1
     2.9    include LEXICON0
    2.10    include SYN_EXT0
    2.11 @@ -500,9 +499,8 @@
    2.12  
    2.13  
    2.14  
    2.15 -(** export parts of internal Syntax structures **)
    2.16 -
    2.17 -open TokenTrans Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    2.18 +(*export parts of internal Syntax structures*)
    2.19 +open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    2.20  
    2.21  end;
    2.22  
     3.1 --- a/src/Pure/Syntax/type_ext.ML	Sat Apr 23 19:51:11 2005 +0200
     3.2 +++ b/src/Pure/Syntax/type_ext.ML	Sat Apr 23 19:51:24 2005 +0200
     3.3 @@ -220,7 +220,7 @@
     3.4     [],
     3.5     [],
     3.6     map SynExt.mk_trfun [("fun", fun_ast_tr')])
     3.7 -  TokenTrans.token_translation
     3.8 +  (map (fn s => ("", s, Output.output_width)) SynExt.standard_token_classes)
     3.9    ([], []);
    3.10  
    3.11  end;