NEWS
changeset 16860 43abdba4da5c
parent 16856 6468a5d6a16e
child 16868 eaafda56b14c
equal deleted inserted replaced
16859:8ac6d4902b56 16860:43abdba4da5c
   376 that of the SML basis, which has constructors NONE and SOME instead of
   376 that of the SML basis, which has constructors NONE and SOME instead of
   377 None and Some, as well as exception Option.Option instead of OPTION.
   377 None and Some, as well as exception Option.Option instead of OPTION.
   378 The functions the, if_none, is_some, is_none have been adapted
   378 The functions the, if_none, is_some, is_none have been adapted
   379 accordingly, while Option.map replaces apsome.
   379 accordingly, while Option.map replaces apsome.
   380 
   380 
   381 * The exception LIST has been given up in favour of the standard
   381 * Pure/library.ML: the exception LIST has been given up in favour of
   382 exceptions Empty and Subscript, as well as Library.UnequalLengths.
   382 the standard exceptions Empty and Subscript, as well as
   383 Function like Library.hd and Library.tl are superceded by the standard
   383 Library.UnequalLengths.  Function like Library.hd and Library.tl are
   384 hd and tl functions etc.
   384 superceded by the standard hd and tl functions etc.
   385 
   385 
   386 A number of basic functions are now no longer exported to the ML
   386 A number of basic list functions are no longer exported to the ML
   387 toplevel, as they are variants of standard functions.  The following
   387 toplevel, as they are variants of predefined functions.  The following
   388 suggests how one can translate existing code:
   388 suggests how one can translate existing code:
   389 
   389 
   390     rev_append xs ys = List.revAppend (xs, ys)
   390     rev_append xs ys = List.revAppend (xs, ys)
   391     nth_elem (i, xs) = List.nth (xs, i)
   391     nth_elem (i, xs) = List.nth (xs, i)
   392     last_elem xs = List.last xs
   392     last_elem xs = List.last xs
   393     flat xss = List.concat xss
   393     flat xss = List.concat xss
   394     seq fs = List.app fs
   394     seq fs = List.app fs
   395     partition P xs = List.partition P xs
   395     partition P xs = List.partition P xs
   396     filter P xs = List.filter P xs
       
   397     mapfilter f xs = List.mapPartial f xs
   396     mapfilter f xs = List.mapPartial f xs
       
   397 
       
   398 * Pure/library.ML: several combinators for linear functional
       
   399 transformations, notably reverse application and composition:
       
   400 
       
   401   x |> f		f #> g
       
   402   (x, y) |-> f		f #-> g
       
   403 
       
   404 * Pure/library.ML: canonical list combinators fold, fold_rev, and
       
   405 fold_yield support linear functional transformations and nesting.  For
       
   406 example:
       
   407 
       
   408   fold f [x1, ..., xN] y =
       
   409     y |> f x1 |> ... |> f xN
       
   410 
       
   411   (fold o fold) f [xs1, ..., xsN] y =
       
   412     y |> fold f xs1 |> ... |> fold f xsN
       
   413 
       
   414   fold f [x1, ..., xN] =
       
   415     f x1 #> ... #> f xN
       
   416 
       
   417   (fold o fold) f [xs1, ..., xsN] =
       
   418     fold f xs1 #> ... #> fold f xsN
       
   419 
       
   420 * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
       
   421 fold_types traverse types/terms from left to right, observing
       
   422 canonical argument order.  Supercedes previous foldl_XXX versions,
       
   423 add_frees, add_vars have been adapted as well: INCOMPATIBILITY.
   398 
   424 
   399 * Pure: output via the Isabelle channels of writeln/warning/error
   425 * Pure: output via the Isabelle channels of writeln/warning/error
   400 etc. is now passed through Output.output, with a hook for arbitrary
   426 etc. is now passed through Output.output, with a hook for arbitrary
   401 transformations depending on the print_mode (cf. Output.add_mode --
   427 transformations depending on the print_mode (cf. Output.add_mode --
   402 the first active mode that provides a output function wins).  Already
   428 the first active mode that provides a output function wins).  Already