#
2608d12d |
|
03-Sep-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Promote Isabelle's Exn.reraise to Portable This function keeps Poly/ML's location information from the original exception intact (otherwise, the location information given to it is that of the new raise). Under Moscow ML, there is no location information so reraise is just equal to raise.
|
#
19626c96 |
|
03-Sep-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Promote more Isabelle concurrency code Portable gets slightly richer with make_counter : {inc:int,init:int} -> unit -> int syncref : 'a -> {get:unit->'a, upd : ('a -> 'b * 'a) -> 'b} Under Moscow ML these map to obvious operations on references. Under Poly/ML these map to synchronised variables that are operated on atomically.
|
#
81c8a834 |
|
23-Feb-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Better document our use of the Susp code from Moscow ML. Unfortunately, a Moscow ML 2.01 bug (now reported) means we end up having to use a new name (HOLSusp) to get the dependencies working properly. Without this change, building the standard kernel on Moscow ML would always recompile Thm.sml, seemingly because it couldn't see the non-existent Susp.ui in SIGOBJ (this file only appears there in the Poly/ML build). There may still be a Holmake bug here too.
|
#
f4b51e0c |
|
18-Dec-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Moved a bunch of things from tools-poly/poly to portableML/poly. Still to do: make Poly Arb{int,num} use Poly's built-in arbitrarily large integer type. Also want to get rid of the last remaining "redirect" in tools-poly/poly/poly-init2.ML.
|
#
38a45f52 |
|
18-Dec-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Reorder the initial build sequence so implementation specific files come 1st. This will make fiddling with the Poly/ML build easier.
|