[isabelle-dev] CVS

[Amine Chaieb]

Hi,

I have just updated my sources and Pure does not compile on OS X. I get 
the message :

Pure FAILED
(see also /Users/chaieb/isabelle/heaps//polyml-5.2_ppc-darwin/log/Pure)

{getChar = get, putString = put, lineNumber = fn ... => ..., fileName = 
name,
   nameSpace = ...}

Error: in 'ML-Systems/polyml.ML', line 39.
Can't unify (unit -> string) * (string -> unit) with
    {getChar: unit -> String.char option, fileName: 'a, nameSpace: bad,
      putString: string -> unit, lineNumber: ...} (Field 1 missing) 
Found near
    while not(List.null(!(in_buffer))) do
    PolyML.compiler({getChar = get, putString = ..., ...})(())


The problem is that the file polyml.ML has no line 39. Any hints? Is 
this Problem known to somebody?

When I use my Older PolyML installation (5.0), Compiling Pure terminates 
in 0 sec without an error message. The log file though contain the 
following:

 > val exit = fn : int -> unit
Error:
Structure (SaveState) has not been declared in structure PolyML
Found near
(
    PolyML.shareCommonData(PolyML.rootFunction);
    TextIO.output
    (
       TextIO.stdOut,
       "Exporting 
/Users/chaieb/isabelle/heaps//polyml-5.1_ppc-darwin/Pure\n"
       )
    ;
    PolyML.SaveState.saveState(
    "/Users/chaieb/isabelle/heaps//polyml-5.1_ppc-darwin/Pure");
    true
    )

Static errors (pass2)
 >


Amine.