explicit Syntax.tokenize, Syntax.parse;

--- a/src/Pure/Syntax/syntax.ML	Wed Apr 06 15:10:39 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Apr 06 15:24:26 2011 +0200
@@ -116,6 +116,8 @@
     prtabs: Printer.prtabs}
   val eq_syntax: syntax * syntax -> bool
   val is_keyword: syntax -> string -> bool
+  val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
+  val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list
   type mode
   val mode_default: mode
   val mode_input: mode
@@ -490,6 +492,8 @@
 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
 
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
+fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
+fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt gram;
 
 type mode = string * bool;
 val mode_default = ("", true);
@@ -770,7 +774,9 @@
 
 
 (*export parts of internal Syntax structures*)
+val syntax_tokenize = tokenize;
 open Lexicon Syn_Ext Type_Ext Syn_Trans Mixfix Printer;
+val tokenize = syntax_tokenize;
 
 end;
 

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 15:10:39 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 15:24:26 2011 +0200
@@ -239,12 +239,13 @@
 
 fun parse_asts ctxt raw root (syms, pos) =
   let
-    val {lexicon, gram, parse_ast_trtab, ...} = Syntax.rep_syntax (ProofContext.syn_of ctxt);
+    val syn = ProofContext.syn_of ctxt;
+    val {parse_ast_trtab, ...} = Syntax.rep_syntax syn;
 
-    val toks = Lexicon.tokenize lexicon raw syms;
+    val toks = Syntax.tokenize syn raw syms;
     val _ = List.app (Lexicon.report_token ctxt) toks;
 
-    val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
+    val pts = Syntax.parse ctxt syn root (filter Lexicon.is_proper toks)
       handle ERROR msg =>
         error (msg ^
           implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));