prevent line breaks after Scala symbolic operators
authorhaftmann
Thu, 26 Aug 2010 12:19:49 +0200
changeset 38773 f9837065b5e8
parent 38772 eb7bc47f062b
child 38774 567b94f8bb6e
prevent line breaks after Scala symbolic operators
src/HOL/HOL.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Library/Code_Integer.thy
src/HOL/ex/Numeral.thy
--- a/src/HOL/HOL.thy	Thu Aug 26 10:23:25 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Aug 26 12:19:49 2010 +0200
@@ -1924,7 +1924,7 @@
   (Haskell "True" and "False" and "not"
     and infixl 3 "&&" and infixl 2 "||"
     and "!(if (_)/ then (_)/ else (_))")
-  (Scala "true" and "false" and "'!/ _"
+  (Scala "true" and "false" and "'! _"
     and infixl 3 "&&" and infixl 1 "||"
     and "!(if ((_))/ (_)/ else (_))")
 
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Aug 26 10:23:25 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Aug 26 12:19:49 2010 +0200
@@ -478,6 +478,7 @@
 
 code_include Scala "Heap"
 {*import collection.mutable.ArraySeq
+
 def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
 
 class Ref[A](x: A) {
--- a/src/HOL/Library/Code_Integer.thy	Thu Aug 26 10:23:25 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Thu Aug 26 12:19:49 2010 +0200
@@ -51,14 +51,14 @@
   (SML "IntInf.- ((_), 1)")
   (OCaml "Big'_int.pred'_big'_int")
   (Haskell "!(_/ -/ 1)")
-  (Scala "!(_/ -/ 1)")
+  (Scala "!(_ -/ 1)")
   (Eval "!(_/ -/ 1)")
 
 code_const Int.succ
   (SML "IntInf.+ ((_), 1)")
   (OCaml "Big'_int.succ'_big'_int")
   (Haskell "!(_/ +/ 1)")
-  (Scala "!(_/ +/ 1)")
+  (Scala "!(_ +/ 1)")
   (Eval "!(_/ +/ 1)")
 
 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
--- a/src/HOL/ex/Numeral.thy	Thu Aug 26 10:23:25 2010 +0200
+++ b/src/HOL/ex/Numeral.thy	Thu Aug 26 12:19:49 2010 +0200
@@ -1033,14 +1033,14 @@
   (SML "IntInf.- ((_), 1)")
   (OCaml "Big'_int.pred'_big'_int")
   (Haskell "!(_/ -/ 1)")
-  (Scala "!(_/ -/ 1)")
+  (Scala "!(_ -/ 1)")
   (Eval "!(_/ -/ 1)")
 
 code_const Int.succ
   (SML "IntInf.+ ((_), 1)")
   (OCaml "Big'_int.succ'_big'_int")
   (Haskell "!(_/ +/ 1)")
-  (Scala "!(_/ +/ 1)")
+  (Scala "!(_ +/ 1)")
   (Eval "!(_/ +/ 1)")
 
 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"