Standard ML of New Jersey v110.68 [built: Sat Dec 27 14:47:23 2008]
!* unable to process `' (unknown extension `<none>')
- [autoloading]
[library $SMLNJ-BASIS/basis.cm is stable]
[autoloading done]
val exit = fn : int -> unit
[autoloading]
[autoloading done]
val commit = fn : unit -> bool
val ml_system = "smlnj-110" : string
val ml_platform = "x86-linux" : string
[opening ML-Systems/smlnj.ML]
[opening ML-Systems/proper_int.ML]
val ml_system_fix_ints = true : bool
[autoloading]
[autoloading done]
val mk_int = fn : int -> IntInf.int
val dest_int = fn : IntInf.int -> int
structure OrigInt : INTEGER
structure OrigIntInf : INT_INF
type int = int
structure IntInf :
  sig
    type int = int
    val precision : Int31.int option
    val minInt : int option
    val maxInt : int option
    val toLarge : int -> int
    val fromLarge : int -> int
    val ~ : int -> int
    val + : int * int -> int
    val - : int * int -> int
    val * : int * int -> int
    val div : int * int -> int
    val mod : int * int -> int
    val quot : int * int -> int
    val rem : int * int -> int
    val min : int * int -> int
    val max : int * int -> int
    val abs : int -> int
    val sameSign : int * int -> bool
    val > : int * int -> bool
    val >= : int * int -> bool
    val < : int * int -> bool
    val <= : int * int -> bool
    val compare : int * int -> order
    val toString : int -> string
    val fromString : string -> int option
    val scan : StringCvt.radix
               -> (char,'a) StringCvt.reader -> (int,'a) StringCvt.reader
    val fmt : StringCvt.radix -> int -> string
    val divMod : int * int -> int * int
    val quotRem : int * int -> int * int
    val pow : int * Int31.int -> int
    val orb : int * int -> int
    val xorb : int * int -> int
    val andb : int * int -> int
    val notb : int -> int
    val << : int * word -> int
    val ~>> : int * word -> int
    val fromInt : int -> int
    val toInt : int -> int
    val log2 : int -> int
    val sign : int -> int
  end
structure Int :
  sig
    type int = int
    val precision : Int31.int option
    val minInt : int option
    val maxInt : int option
    val toLarge : int -> int
    val fromLarge : int -> int
    val ~ : int -> int
    val + : int * int -> int
    val - : int * int -> int
    val * : int * int -> int
    val div : int * int -> int
    val mod : int * int -> int
    val quot : int * int -> int
    val rem : int * int -> int
    val min : int * int -> int
    val max : int * int -> int
    val abs : int -> int
    val sameSign : int * int -> bool
    val > : int * int -> bool
    val >= : int * int -> bool
    val < : int * int -> bool
    val <= : int * int -> bool
    val compare : int * int -> order
    val toString : int -> string
    val fromString : string -> int option
    val scan : StringCvt.radix
               -> (char,'a) StringCvt.reader -> (int,'a) StringCvt.reader
    val fmt : StringCvt.radix -> int -> string
    val divMod : int * int -> int * int
    val quotRem : int * int -> int * int
    val pow : int * Int31.int -> int
    val orb : int * int -> int
    val xorb : int * int -> int
    val andb : int * int -> int
    val notb : int -> int
    val << : int * word -> int
    val ~>> : int * word -> int
    val fromInt : int -> int
    val toInt : int -> int
    val log2 : int -> int
    val sign : int -> int
  end
[autoloading]
[autoloading done]
structure List :
  sig
    datatype 'a list = :: of 'a * 'a list | nil
    exception Empty
    val null : 'a list -> bool
    val hd : 'a list -> 'a
    val tl : 'a list -> 'a list
    val last : 'a list -> 'a
    val getItem : 'a list -> ('a * 'a list) option
    val rev : 'a list -> 'a list
    val @ : 'a list * 'a list -> 'a list
    val concat : 'a list list -> 'a list
    val revAppend : 'a list * 'a list -> 'a list
    val app : ('a -> unit) -> 'a list -> unit
    val map : ('a -> 'b) -> 'a list -> 'b list
    val mapPartial : ('a -> 'b option) -> 'a list -> 'b list
    val find : ('a -> bool) -> 'a list -> 'a option
    val filter : ('a -> bool) -> 'a list -> 'a list
    val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
    val foldr : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b
    val foldl : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b
    val exists : ('a -> bool) -> 'a list -> bool
    val all : ('a -> bool) -> 'a list -> bool
    val collate : ('a * 'a -> order) -> 'a list * 'a list -> order
    val length : 'a list -> int
    val nth : 'a list * int -> 'a
    val take : 'a list * int -> 'a list
    val drop : 'a list * int -> 'a list
    val tabulate : int * (int -> 'a) -> 'a list
  end
val length = fn : 'a list -> int
[autoloading]
[autoloading done]
structure Array :
  sig
    type 'a array = 'a array
    type 'a vector = 'a vector
    val fromList : 'a list -> 'a array
    val vector : 'a array -> 'a vector
    val app : ('a -> unit) -> 'a array -> unit
    val modify : ('a -> 'a) -> 'a array -> unit
    val foldl : ('a * 'b -> 'b) -> 'b -> 'a array -> 'b
    val foldr : ('a * 'b -> 'b) -> 'b -> 'a array -> 'b
    val find : ('a -> bool) -> 'a array -> 'a option
    val exists : ('a -> bool) -> 'a array -> bool
    val all : ('a -> bool) -> 'a array -> bool
    val collate : ('a * 'a -> order) -> 'a array * 'a array -> order
    val maxLen : int
    val array : int * 'a -> 'a array
    val tabulate : int * (int -> 'a) -> 'a array
    val length : 'a array -> int
    val sub : 'a array * int -> 'a
    val update : 'a array * int * 'a -> unit
    val copy : {di:int, dst:'a array, src:'a array} -> unit
    val copyVec : {di:int, dst:'a array, src:'a vector} -> unit
    val appi : (int * 'a -> unit) -> 'a array -> unit
    val modifyi : (int * 'a -> 'a) -> 'a array -> unit
    val foldli : (int * 'a * 'b -> 'b) -> 'b -> 'a array -> 'b
    val foldri : (int * 'a * 'b -> 'b) -> 'b -> 'a array -> 'b
    val findi : (int * 'a -> bool) -> 'a array -> (int * 'a) option
  end
[autoloading]
[autoloading done]
structure Vector :
  sig
    type 'a vector = 'a vector
    val fromList : 'a list -> 'a vector
    val concat : 'a vector list -> 'a vector
    val app : ('a -> unit) -> 'a vector -> unit
    val map : ('a -> 'b) -> 'a vector -> 'b vector
    val foldl : ('a * 'b -> 'b) -> 'b -> 'a vector -> 'b
    val foldr : ('a * 'b -> 'b) -> 'b -> 'a vector -> 'b
    val find : ('a -> bool) -> 'a vector -> 'a option
    val exists : ('a -> bool) -> 'a vector -> bool
    val all : ('a -> bool) -> 'a vector -> bool
    val collate : ('a * 'a -> order) -> 'a vector * 'a vector -> order
    val maxLen : int
    val tabulate : int * (int -> 'a) -> 'a vector
    val length : 'a vector -> int
    val sub : 'a vector * int -> 'a
    val update : 'a vector * int * 'a -> 'a vector
    val appi : (int * 'a -> unit) -> 'a vector -> unit
    val mapi : (int * 'a -> 'b) -> 'a vector -> 'b vector
    val foldli : (int * 'a * 'b -> 'b) -> 'b -> 'a vector -> 'b
    val foldri : (int * 'a * 'b -> 'b) -> 'b -> 'a vector -> 'b
    val findi : (int * 'a -> bool) -> 'a vector -> (int * 'a) option
  end
[autoloading]
[autoloading done]
structure Char :
  sig
    type char = char
    type string = string
    val minChar : char
    val maxChar : char
    val pred : char -> char
    val succ : char -> char
    val < : char * char -> bool
    val <= : char * char -> bool
    val > : char * char -> bool
    val >= : char * char -> bool
    val compare : char * char -> order
    val scan : (char,'a) StringCvt.reader -> (char,'a) StringCvt.reader
    val fromString : string -> char option
    val toString : char -> string
    val fromCString : string -> char option
    val toCString : char -> string
    val contains : string -> char -> bool
    val notContains : string -> char -> bool
    val isLower : char -> bool
    val isUpper : char -> bool
    val isDigit : char -> bool
    val isAlpha : char -> bool
    val isHexDigit : char -> bool
    val isAlphaNum : char -> bool
    val isPrint : char -> bool
    val isSpace : char -> bool
    val isPunct : char -> bool
    val isGraph : char -> bool
    val isCntrl : char -> bool
    val isAscii : char -> bool
    val toUpper : char -> char
    val toLower : char -> char
    val maxOrd : int
    val chr : int -> char
    val ord : char -> int
  end
val chr = fn : int -> char
val ord = fn : char -> int
[autoloading]
[autoloading done]
structure String :
  sig
    type char = char
    type string = string
    val ^ : string * string -> string
    val concat : string list -> string
    val concatWith : string -> string list -> string
    val str : char -> string
    val implode : char list -> string
    val explode : string -> char list
    val map : (char -> char) -> string -> string
    val translate : (char -> string) -> string -> string
    val tokens : (char -> bool) -> string -> string list
    val fields : (char -> bool) -> string -> string list
    val isPrefix : string -> string -> bool
    val isSubstring : string -> string -> bool
    val isSuffix : string -> string -> bool
    val compare : string * string -> order
    val collate : (char * char -> order) -> string * string -> order
    val < : string * string -> bool
    val <= : string * string -> bool
    val > : string * string -> bool
    val >= : string * string -> bool
    val fromString : string -> string option
    val toString : string -> string
    val fromCString : string -> string option
    val toCString : string -> string
    val maxSize : int
    val size : string -> int
    val sub : string * int -> char
    val extract : string * int * int option -> string
    val substring : string * int * int -> string
  end
val size = fn : string -> int
val substring = fn : string * int * int -> string
[autoloading]
[autoloading done]
structure Substring :
  sig
    type char = char
    type string = string
    type substring
    val full : string -> substring
    val string : substring -> string
    val isEmpty : substring -> bool
    val getc : substring -> (char * substring) option
    val first : substring -> char option
    val concat : substring list -> string
    val concatWith : string -> substring list -> string
    val explode : substring -> char list
    val isPrefix : string -> substring -> bool
    val isSubstring : string -> substring -> bool
    val isSuffix : string -> substring -> bool
    val compare : substring * substring -> order
    val collate : (char * char -> order) -> substring * substring -> order
    val splitl : (char -> bool) -> substring -> substring * substring
    val splitr : (char -> bool) -> substring -> substring * substring
    val dropl : (char -> bool) -> substring -> substring
    val dropr : (char -> bool) -> substring -> substring
    val takel : (char -> bool) -> substring -> substring
    val taker : (char -> bool) -> substring -> substring
    val position : string -> substring -> substring * substring
    val span : substring * substring -> substring
    val translate : (char -> string) -> substring -> string
    val tokens : (char -> bool) -> substring -> substring list
    val fields : (char -> bool) -> substring -> substring list
    val app : (char -> unit) -> substring -> unit
    val foldl : (char * 'a -> 'a) -> 'a -> substring -> 'a
    val foldr : (char * 'a -> 'a) -> 'a -> substring -> 'a
    val sub : substring * int -> char
    val size : substring -> int
    val base : substring -> string * int * int
    val extract : string * int * int option -> substring
    val substring : string * int * int -> substring
    val triml : int -> substring -> substring
    val trimr : int -> substring -> substring
    val slice : substring * int * int option -> substring
    val splitAt : substring * int -> substring * substring
  end
[autoloading]
[autoloading done]
structure Word :
  sig
    type word = word
    val toLarge : word -> Word32.word
    val toLargeX : word -> Word32.word
    val fromLarge : Word32.word -> word
    val toLargeWord : word -> Word32.word
    val toLargeWordX : word -> Word32.word
    val fromLargeWord : Word32.word -> word
    val toLargeInt : word -> int
    val toLargeIntX : word -> int
    val fromLargeInt : int -> word
    val orb : word * word -> word
    val xorb : word * word -> word
    val andb : word * word -> word
    val notb : word -> word
    val << : word * word -> word
    val >> : word * word -> word
    val ~>> : word * word -> word
    val + : word * word -> word
    val - : word * word -> word
    val * : word * word -> word
    val div : word * word -> word
    val mod : word * word -> word
    val compare : word * word -> order
    val > : word * word -> bool
    val >= : word * word -> bool
    val < : word * word -> bool
    val <= : word * word -> bool
    val ~ : word -> word
    val min : word * word -> word
    val max : word * word -> word
    val scan : StringCvt.radix
               -> (char,'a) StringCvt.reader -> (word,'a) StringCvt.reader
    val fromString : string -> word option
    val fmt : StringCvt.radix -> word -> string
    val toString : word -> string
    val wordSize : int
    val toInt : word -> int
    val toIntX : word -> int
    val fromInt : int -> word
  end
[autoloading]
[autoloading done]
structure Real :
  sig
    type real = real
    structure Math : <sig>
    val maxFinite : real
    val minPos : real
    val minNormalPos : real
    val posInf : real
    val negInf : real
    val + : real * real -> real
    val - : real * real -> real
    val * : real * real -> real
    val / : real * real -> real
    val *+ : real * real * real -> real
    val *- : real * real * real -> real
    val ~ : real -> real
    val abs : real -> real
    val min : real * real -> real
    val max : real * real -> real
    val signBit : real -> bool
    val sameSign : real * real -> bool
    val copySign : real * real -> real
    val compare : real * real -> order
    val compareReal : real * real -> IEEEReal.real_order
    val < : real * real -> bool
    val <= : real * real -> bool
    val > : real * real -> bool
    val >= : real * real -> bool
    val == : real * real -> bool
    val != : real * real -> bool
    val ?= : real * real -> bool
    val unordered : real * real -> bool
    val isFinite : real -> bool
    val isNan : real -> bool
    val isNormal : real -> bool
    val class : real -> IEEEReal.float_class
    val fmt : StringCvt.realfmt -> real -> string
    val toString : real -> string
    val fromString : string -> real option
    val scan : (char,'a) StringCvt.reader -> (real,'a) StringCvt.reader
    val split : real -> {frac:real, whole:real}
    val realMod : real -> real
    val rem : real * real -> real
    val nextAfter : real * real -> real
    val checkFloat : real -> real
    val realFloor : real -> real
    val realCeil : real -> real
    val realTrunc : real -> real
    val realRound : real -> real
    val toLargeInt : IEEEReal.rounding_mode -> real -> int
    val fromLargeInt : int -> real
    val toLarge : real -> real
    val fromLarge : IEEEReal.rounding_mode -> real -> real
    val toDecimal : real -> IEEEReal.decimal_approx
    val fromDecimal : IEEEReal.decimal_approx -> real
    val radix : int
    val precision : int
    val sign : real -> int
    val toManExp : real -> {exp:int, man:real}
    val fromManExp : {exp:int, man:real} -> real
    val ceil : real -> int
    val floor : real -> int
    val real : int -> real
    val round : real -> int
    val trunc : real -> int
    val toInt : IEEEReal.rounding_mode -> real -> int
    val fromInt : int -> real
  end
val ceil = fn : real -> int
val floor = fn : real -> int
val real = fn : int -> real
val round = fn : real -> int
val trunc = fn : real -> int
[autoloading]
[autoloading done]
structure TextIO :
  sig
    type vector = string
    type elem = char
    type instream
    type outstream
    val input : instream -> vector
    val input1 : instream -> elem option
    val inputAll : instream -> vector
    val lookahead : instream -> elem option
    val closeIn : instream -> unit
    val endOfStream : instream -> bool
    val output : outstream * vector -> unit
    val output1 : outstream * elem -> unit
    val flushOut : outstream -> unit
    val closeOut : outstream -> unit
    structure StreamIO : <sig>
    val mkInstream : ?.TextIO.instream -> instream
    val getInstream : instream -> ?.TextIO.instream
    val setInstream : instream * ?.TextIO.instream -> unit
    val getPosOut : outstream -> ?.TextIO.out_pos
    val setPosOut : outstream * ?.TextIO.out_pos -> unit
    val mkOutstream : ?.TextIO.outstream -> outstream
    val getOutstream : outstream -> ?.TextIO.outstream
    val setOutstream : outstream * ?.TextIO.outstream -> unit
    val inputLine : instream -> string option
    val outputSubstr : outstream * substring -> unit
    val openIn : string -> instream
    val openString : string -> instream
    val openOut : string -> outstream
    val openAppend : string -> outstream
    val stdIn : instream
    val stdOut : outstream
    val stdErr : outstream
    val print : string -> unit
    val scanStream : ((elem,?.TextIO.instream) StringCvt.reader
                      -> ('a,?.TextIO.instream) StringCvt.reader)
                     -> instream -> 'a option
    val inputN : instream * int -> vector
    val canInput : instream * int -> int option
  end
[autoloading]
[autoloading done]
structure Time :
  sig
    datatype time = ...
    exception Time
    val zeroTime : time
    val fromReal : real -> time
    val toReal : time -> real
    val toSeconds : time -> int
    val fromSeconds : int -> time
    val toMilliseconds : time -> int
    val fromMilliseconds : int -> time
    val toMicroseconds : time -> int
    val fromMicroseconds : int -> time
    val toNanoseconds : time -> int
    val fromNanoseconds : int -> time
    val + : time * time -> time
    val - : time * time -> time
    val compare : time * time -> order
    val < : time * time -> bool
    val <= : time * time -> bool
    val > : time * time -> bool
    val >= : time * time -> bool
    val now : unit -> time
    val toString : time -> string
    val fromString : string -> time option
    val scan : (char,'a) StringCvt.reader -> (time,'a) StringCvt.reader
    val fmt : int -> time -> string
  end
[autoloading]
[autoloading done]
structure Posix :
  sig
    structure Error : <sig>
    structure Signal : <sig>
    structure Process : <sig>
    structure ProcEnv : <sig>
    structure FileSys : <sig>
    structure SysDB : <sig>
    structure TTY : <sig>
    structure IO : <sig>
  end
val it = () : unit
[opening ML-Systems/overloading_smlnj.ML]
[autoloading]
[library $smlnj/compiler/current.cm is stable]
[library $smlnj/compiler/x86.cm is stable]
[library $smlnj/viscomp/core.cm is stable]
[library $smlnj/viscomp/basics.cm is stable]
[library $smlnj/viscomp/elabdata.cm is stable]
[library $smlnj/viscomp/elaborate.cm is stable]
[library $smlnj/MLRISC/MLRISC.cm is stable]
[library $SMLNJ-MLRISC/MLRISC.cm is stable]
[library $smlnj-lib.cm(=$SMLNJ-LIB/Util)/smlnj-lib.cm is stable]
[library $Graphs.cm(=$SMLNJ-MLRISC)/Graphs.cm is stable]
[library $Lib.cm(=$SMLNJ-MLRISC)/Lib.cm is stable]
[library $smlnj/viscomp/debugprof.cm is stable]
[library $smlnj/MLRISC/Control.cm is stable]
[library $SMLNJ-MLRISC/Control.cm is stable]
[library $controls-lib.cm(=$SMLNJ-LIB/Controls)/controls-lib.cm is stable]
[library $smlnj/smlnj-lib/controls-lib.cm is stable]
[autoloading done]
val it = () : unit
[autoloading]
[autoloading done]
overload
overload
overload
overload
overload
overload
overload
overload
overload
overload
overload
val it = () : unit
val it = () : unit
[opening ML-Systems/exn.ML]
structure Exn :
  sig
    datatype 'a result = Exn of exn | Result of 'a
    val get_result : 'a result -> 'a option
    val get_exn : 'a result -> exn option
    val capture : ('a -> 'b) -> 'a -> 'b result
    val release : 'a result -> 'a
    exception EXCEPTIONS of exn list * string
  end
val it = () : unit
[opening ML-Systems/universal.ML]
signature UNIVERSAL =
  sig
    type universal
    type 'a tag
    val tag : unit -> 'a tag
    val tagIs : 'a tag -> universal -> bool
    val tagInject : 'a tag -> 'a -> universal
    val tagProject : 'a tag -> universal -> 'a
  end
ML-Systems/universal.ML:34.15-34.34 Warning: match nonexhaustive
          Universal x => ...
  
structure Universal : UNIVERSAL
val it = () : unit
[opening ML-Systems/multithreading.ML]
signature BASIC_MULTITHREADING =
  sig
    val NAMED_CRITICAL : string -> (unit -> 'a) -> 'a
    val CRITICAL : (unit -> 'a) -> 'a
  end
signature MULTITHREADING =
  sig
    val NAMED_CRITICAL : string -> (unit -> 'a) -> 'a
    val CRITICAL : (unit -> 'a) -> 'a
    val trace : int ref
    val tracing : int -> (unit -> string) -> unit
    val available : bool
    val max_threads : int ref
    val max_threads_value : unit -> int
    val self_critical : unit -> bool
    datatype 'a task
      = Task of {body:unit -> unit, cont:'a -> 'a, fail:'a -> 'a}
      | Terminate
      | Wait
    val schedule : int -> ('a -> 'a task * 'a) -> 'a -> exn list
    val serial : unit -> int
    val get_data : 'a Universal.tag -> 'a option
    val put_data : 'a Universal.tag * 'a -> unit
  end
structure Multithreading : MULTITHREADING
structure BasicMultithreading : BASIC_MULTITHREADING
opening BasicMultithreading
  val NAMED_CRITICAL : string -> (unit -> 'a) -> 'a
  val CRITICAL : (unit -> 'a) -> 'a
val it = () : unit
[opening ML-Systems/system_shell.ML]
[autoloading]
[autoloading done]
val system_out = fn : TextIO.vector -> TextIO.vector * ?.int
val it = () : unit
[autoloading]
[library $smlnj/cm/cm.cm is stable]
[library $smlnj/internal/cm-sig-lib.cm is stable]
[library $/pgraph.cm is stable]
[library $smlnj/internal/srcpath-lib.cm is stable]
[autoloading done]
val it = true : bool
[autoloading]
[autoloading done]
val pointer_eq = fn : 'a * 'a -> bool
[autoloading]
[autoloading done]
val ord = fn : string -> int
val chr = fn : int -> string
val explode = fn : string -> string list
val implode = fn : string list -> string
val exit = fn : int -> unit
val quit = fn : unit -> unit
val get_print_depth = fn : unit -> int
val print_depth = fn : int -> unit
[autoloading]
[autoloading done]
val start_timing = fn
  : unit -> Timer.cpu_timer * {sys:Time.time, usr:Time.time}
val end_timing = fn
  : Timer.cpu_timer * {sys:Time.time, usr:Time.time} -> string
val check_timer = fn : Timer.cpu_timer -> Time.time * Time.time * Time.time
val ml_prompts = fn : string -> string -> unit
val profile = fn : int -> ('a -> 'b) -> 'a -> 'b
val exception_trace = fn : (unit -> 'a) -> 'a
val print = fn : 'a -> 'a
val makestring = fn : 'a -> string
[autoloading]
[library $smlnj/smlnj-lib/pp-lib.cm is stable]
[library $SMLNJ-LIB/PP/pp-lib.cm is stable]
[library $html-lib.cm(=$SMLNJ-LIB/HTML)/html-lib.cm is stable]
[autoloading done]
val make_pp = fn
  : 'a
    -> ('b
        -> (string -> unit) * (int -> unit) * (int -> unit) * (unit -> unit)
           * (unit -> unit)
           -> 'c)
       -> 'a * (?.PrettyPrint.PP.stream -> 'b -> 'c)
[autoloading]
[autoloading done]
val install_pp = fn
  : string list * (?.PrettyPrint.PP.stream -> 'a -> unit) -> unit
[autoloading]
[library $smlnj/MLRISC/IA32.cm is stable]
[library $SMLNJ-MLRISC/IA32.cm is stable]
Error: Compiler bug: UnpickMod: stub lookup failed
Expected to find ML heap file /home/tim/programming/downloaded/Isabelle2008/heaps/smlnj-110_x86-linux/Pure.x86-linux