# HG changeset patch # User wenzelm # Date 850218666 -3600 # Node ID 74c99949ad84c898f7e8b0924b3093db20aac8fc # Parent 1b6bc618c35600d13fb41e6bb1e86032f9747cca *** empty log message *** diff -r 1b6bc618c356 -r 74c99949ad84 src/Pure/Syntax/ROOT.ML --- a/src/Pure/Syntax/ROOT.ML Tue Dec 10 12:50:35 1996 +0100 +++ b/src/Pure/Syntax/ROOT.ML Tue Dec 10 12:51:06 1996 +0100 @@ -5,9 +5,10 @@ This file builds the syntax module. *) -use "symbol_font.ML"; use "pretty.ML"; use "lexicon.ML"; +structure Scanner: SCANNER = Lexicon; +use "symbol_font.ML"; use "ast.ML"; use "syn_ext.ML"; use "parser.ML"; @@ -17,8 +18,6 @@ use "printer.ML"; use "syntax.ML"; -(*Hiding: only the most basic features are opened*) +(*hiding: only the most basic features are opened*) structure BasicSyntax: BASIC_SYNTAX = Syntax; open BasicSyntax; - -structure Scanner: SCANNER = Lexicon;