tuned;
authorwenzelm
Wed Apr 16 17:40:40 2008 +0200 (2008-04-16)
changeset 266840701201def95
parent 26683 849281658859
child 26685 40aefd1e8f05
tuned;
src/Pure/General/yxml.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/General/yxml.ML	Wed Apr 16 17:40:39 2008 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Wed Apr 16 17:40:40 2008 +0200
     1.3 @@ -101,7 +101,7 @@
     1.4  (* parsing *)
     1.5  
     1.6  fun parse_attrib s =
     1.7 -  (case String.fields (is_char "=") s of
     1.8 +  (case space_explode "=" s of
     1.9      [] => err_attribute ()
    1.10    | "" :: _ => err_attribute ()
    1.11    | a :: xs => (a, space_implode "=" xs));
     2.1 --- a/src/Pure/Syntax/syntax.ML	Wed Apr 16 17:40:39 2008 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Apr 16 17:40:40 2008 +0200
     2.3 @@ -835,11 +835,13 @@
     2.4    fn x => pretty_arity ctxt x);
     2.5  
     2.6  (*educated guess for reconstructing infixes*)
     2.7 -fun guess_infix (Syntax (syn, _)) c = case Parser.guess_infix_lr (#gram syn) c
     2.8 - of SOME (s, l, r, j) => SOME (if l then Mixfix.InfixlName (s, j)
     2.9 +fun guess_infix (Syntax ({gram, ...}, _)) c =
    2.10 +  (case Parser.guess_infix_lr gram c of
    2.11 +    SOME (s, l, r, j) => SOME
    2.12 +     (if l then Mixfix.InfixlName (s, j)
    2.13        else if r then Mixfix.InfixrName (s, j)
    2.14        else Mixfix.InfixName (s, j))
    2.15 -  | NONE => NONE
    2.16 +  | NONE => NONE);
    2.17  
    2.18  (*export parts of internal Syntax structures*)
    2.19  open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    2.20 @@ -849,11 +851,10 @@
    2.21  structure BasicSyntax: BASIC_SYNTAX = Syntax;
    2.22  open BasicSyntax;
    2.23  
    2.24 -structure Hidden = struct end;
    2.25 -structure Ast = Hidden;
    2.26 -structure SynExt = Hidden;
    2.27 -structure Parser = Hidden;
    2.28 -structure TypeExt = Hidden;
    2.29 -structure SynTrans = Hidden;
    2.30 -structure Mixfix = Hidden;
    2.31 -structure Printer = Hidden;
    2.32 +forget_structure "Ast";
    2.33 +forget_structure "SynExt";
    2.34 +forget_structure "Parser";
    2.35 +forget_structure "TypeExt";
    2.36 +forget_structure "SynTrans";
    2.37 +forget_structure "Mixfix";
    2.38 +forget_structure "Printer";