# HG changeset patch
# User wenzelm
# Date 1392745427 -3600
# Node ID 9c16317c91d1a21463851d734a8f598664a995d1
# Parent  d77090e07000fb96de0d7c1f8838a0647e1025ca
prefer concrete list append;

diff -r d77090e07000 -r 9c16317c91d1 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue Feb 18 18:43:31 2014 +0100
+++ b/src/Pure/General/path.scala	Tue Feb 18 18:43:47 2014 +0100
@@ -94,7 +94,7 @@
       else (List(root_elem(es.head)), es.tail)
     val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
 
-    new Path(norm_elems(elems.reverse ++ roots))
+    new Path(norm_elems(elems.reverse ::: roots))
   }
 
   def is_ok(str: String): Boolean =
diff -r d77090e07000 -r 9c16317c91d1 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Tue Feb 18 18:43:31 2014 +0100
+++ b/src/Pure/General/position.scala	Tue Feb 18 18:43:47 2014 +0100
@@ -50,7 +50,7 @@
 
   object Range
   {
-    def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
+    def apply(range: Text.Range): T = Offset(range.start) ::: Offset(range.stop)
     def unapply(pos: T): Option[Text.Range] =
       (pos, pos) match {
         case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
diff -r d77090e07000 -r 9c16317c91d1 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Feb 18 18:43:31 2014 +0100
+++ b/src/Pure/System/isabelle_system.scala	Tue Feb 18 18:43:47 2014 +0100
@@ -267,7 +267,7 @@
   def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
   {
     val cmdline =
-      if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ++ args
+      if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ::: args.toList
       else args
     val env1 = if (env == null) settings else settings ++ env
     raw_execute(cwd, env1, redirect, cmdline: _*)
@@ -283,7 +283,7 @@
   {
     private val params =
       List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
-    private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)
+    private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*)
 
 
     // channels
@@ -414,7 +414,7 @@
     } match {
       case Some(dir) =>
         val file = standard_path(dir + Path.basic(name))
-        process_output(execute(true, (List(file) ++ args): _*))
+        process_output(execute(true, (List(file) ::: args.toList): _*))
       case None => ("Unknown Isabelle tool: " + name, 2)
     }
   }
diff -r d77090e07000 -r 9c16317c91d1 src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Tue Feb 18 18:43:31 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala	Tue Feb 18 18:43:47 2014 +0100
@@ -80,7 +80,7 @@
     }
   }
 
-  val all_answers = Answer.step.all ++ Answer.hint_fail.all
+  val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all
 
   object Active
   {