# HG changeset patch
# User haftmann
# Date 1282911907 -7200
# Node ID 4d575fbfc920e3aa649eb1d82a537235d6ca2d32
# Parent  f50f0802ba997328393a39dab005393554009c4b
official support for Scala

diff -r f50f0802ba99 -r 4d575fbfc920 NEWS
--- a/NEWS	Fri Aug 27 14:24:26 2010 +0200
+++ b/NEWS	Fri Aug 27 14:25:07 2010 +0200
@@ -40,6 +40,9 @@
 
 *** HOL ***
 
+* Scala (2.8 or higher) has been added to the target languages of
+the code generator.
+
 * Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
 
 * Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
diff -r f50f0802ba99 -r 4d575fbfc920 doc-src/Codegen/Thy/Introduction.thy
--- a/doc-src/Codegen/Thy/Introduction.thy	Fri Aug 27 14:24:26 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy	Fri Aug 27 14:25:07 2010 +0200
@@ -8,8 +8,9 @@
   This tutorial introduces the code generator facilities of @{text
   "Isabelle/HOL"}.  It allows to turn (a certain class of) HOL
   specifications into corresponding executable code in the programming
-  languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml} and
-  @{text Haskell} \cite{haskell-revised-report}.
+  languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml},
+  @{text Haskell} \cite{haskell-revised-report} and @{text Scala}
+  \cite{scala-overview-tech-report}.
 
   To profit from this tutorial, some familiarity and experience with
   @{theory HOL} \cite{isa-tutorial} and its basic theories is assumed.
@@ -78,8 +79,8 @@
   target language identifier and a freely chosen module name.  A file
   name denotes the destination to store the generated code.  Note that
   the semantics of the destination depends on the target language: for
-  @{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text
-  Haskell} it denotes a \emph{directory} where a file named as the
+  @{text SML}, @{text OCaml} and @{text Scala} it denotes a \emph{file},
+  for @{text Haskell} it denotes a \emph{directory} where a file named as the
   module name (with extension @{text ".hs"}) is written:
 *}
 
diff -r f50f0802ba99 -r 4d575fbfc920 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Aug 27 14:24:26 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Aug 27 14:25:07 2010 +0200
@@ -968,7 +968,8 @@
 
   \medskip One framework generates code from functional programs
   (including overloading using type classes) to SML \cite{SML}, OCaml
-  \cite{OCaml} and Haskell \cite{haskell-revised-report}.
+  \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
+  \cite{scala-overview-tech-report}.
   Conceptually, code generation is split up in three steps:
   \emph{selection} of code theorems, \emph{translation} into an
   abstract executable view and \emph{serialization} to a specific
@@ -1015,7 +1016,7 @@
     class: nameref
     ;
 
-    target: 'OCaml' | 'SML' | 'Haskell'
+    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
     ;
 
     'code' ( 'del' | 'abstype' | 'abstract' ) ?
@@ -1088,7 +1089,7 @@
   after the @{keyword "module_name"} keyword; then \emph{all} code is
   placed in this module.
 
-  For \emph{SML} and \emph{OCaml}, the file specification refers to a
+  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
   single file; for \emph{Haskell}, it refers to a whole directory,
   where code is generated in multiple files reflecting the module
   hierarchy.  Omitting the file specification denotes standard
diff -r f50f0802ba99 -r 4d575fbfc920 doc-src/manual.bib
--- a/doc-src/manual.bib	Fri Aug 27 14:24:26 2010 +0200
+++ b/doc-src/manual.bib	Fri Aug 27 14:25:07 2010 +0200
@@ -984,6 +984,14 @@
 
 %O
 
+@TechReport{scala-overview-tech-report,
+  author =       {Martin Odersky and al.},
+  title =        {An Overview of the Scala Programming Language},
+  institution =  {EPFL Lausanne, Switzerland},
+  year =         2004,
+  number =       {IC/2004/64}
+}
+
 @Manual{pvs-language,
   title		= {The {PVS} specification language},
   author	= {S. Owre and N. Shankar and J. M. Rushby},