# HG changeset patch
# User wenzelm
# Date 1330029551 -3600
# Node ID 5949ad86dc9a287bd447f9edd13564a96aa13704
# Parent  2c5c003cee35fd6165caf5653e295d3f261333a6# Parent  e1bdcbe04b8383269ce1d974bcffc45bcf7dec23
merged

diff -r 2c5c003cee35 -r 5949ad86dc9a doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Feb 23 20:33:35 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Feb 23 21:39:11 2012 +0100
@@ -1648,7 +1648,7 @@
   \end{matharray}
 
   @{rail "
-    @@{command (HOL) value} ( '[' name ']' )? modes? @{syntax term}
+    @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
     ;
 
     @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
@@ -1662,11 +1662,11 @@
       @@{command (HOL) nitpick_params}) ( '[' args ']' )?
     ;
 
-    @@{command (HOL) quickcheck_generator} typeconstructor \\
+    @@{command (HOL) quickcheck_generator} @{syntax nameref} \\
       'operations:' ( @{syntax term} +)
     ;
 
-    @@{command (HOL) find_unused_assms} theoryname?
+    @@{command (HOL) find_unused_assms} @{syntax name}?
     ;
 
     modes: '(' (@{syntax name} +) ')'
diff -r 2c5c003cee35 -r 5949ad86dc9a doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Feb 23 20:33:35 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Feb 23 21:39:11 2012 +0100
@@ -2351,7 +2351,7 @@
 \rail@bar
 \rail@nextbar{1}
 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
-\rail@nont{\isa{name}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
 \rail@endbar
 \rail@bar
@@ -2408,7 +2408,7 @@
 \rail@end
 \rail@begin{4}{}
 \rail@term{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}}[]
-\rail@nont{\isa{typeconstructor}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
 \rail@cr{2}
 \rail@term{\isa{operations{\isaliteral{3A}{\isacharcolon}}}}[]
 \rail@plus
@@ -2420,7 +2420,7 @@
 \rail@term{\hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}}}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\isa{theoryname}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@endbar
 \rail@end
 \rail@begin{2}{\isa{modes}}
diff -r 2c5c003cee35 -r 5949ad86dc9a src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Thu Feb 23 20:33:35 2012 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Thu Feb 23 21:39:11 2012 +0100
@@ -249,9 +249,9 @@
   by hoare auto
 
 
-subsection{* Time *}
+subsection {* Time *}
 
-text{* A simple embedding of time in Hoare logic: function @{text
+text {* A simple embedding of time in Hoare logic: function @{text
   timeit} inserts an extra variable to keep track of the elapsed time. *}
 
 record tstate = time :: nat
diff -r 2c5c003cee35 -r 5949ad86dc9a src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Thu Feb 23 20:33:35 2012 +0100
+++ b/src/Pure/General/graph.scala	Thu Feb 23 21:39:11 2012 +0100
@@ -17,7 +17,8 @@
   class Undefined[Key](x: Key) extends Exception
   class Cycles[Key](cycles: List[List[Key]]) extends Exception
 
-  def empty[Key, A]: Graph[Key, A] = new Graph[Key, A](Map.empty)
+  private val empty_val: Graph[Any, Nothing] = new Graph[Any, Nothing](Map.empty)
+  def empty[Key, A]: Graph[Key, A] = empty_val.asInstanceOf[Graph[Key, A]]
 }
 
 
diff -r 2c5c003cee35 -r 5949ad86dc9a src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Thu Feb 23 20:33:35 2012 +0100
+++ b/src/Pure/General/linear_set.scala	Thu Feb 23 21:39:11 2012 +0100
@@ -14,16 +14,10 @@
 
 object Linear_Set extends ImmutableSetFactory[Linear_Set]
 {
-  protected case class Rep[A](
-    val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
-
-  private def empty_rep[A] = Rep[A](None, None, Map(), Map())
-
-  private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A])
-    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(start, end, nexts, prevs) }
+  private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
+  override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]]
 
   implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
-  override def empty[A] = new Linear_Set[A]
 
   class Duplicate[A](x: A) extends Exception
   class Undefined[A](x: A) extends Exception
@@ -31,7 +25,8 @@
 }
 
 
-class Linear_Set[A]
+class Linear_Set[A] private(
+    start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
   extends scala.collection.immutable.Set[A]
   with GenericSetTemplate[A, Linear_Set]
   with SetLike[A, Linear_Set[A]]
@@ -39,20 +34,15 @@
   override def companion: GenericCompanion[Linear_Set] = Linear_Set
 
 
-  /* representation */
-
-  protected val rep = Linear_Set.empty_rep[A]
-
-
   /* relative addressing */
 
   // FIXME check definedness??
-  def next(elem: A): Option[A] = rep.nexts.get(elem)
-  def prev(elem: A): Option[A] = rep.prevs.get(elem)
+  def next(elem: A): Option[A] = nexts.get(elem)
+  def prev(elem: A): Option[A] = prevs.get(elem)
 
   def get_after(hook: Option[A]): Option[A] =
     hook match {
-      case None => rep.start
+      case None => start
       case Some(elem) =>
         if (!contains(elem)) throw new Linear_Set.Undefined(elem)
         next(elem)
@@ -63,51 +53,51 @@
     else
       hook match {
         case None =>
-          rep.start match {
-            case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
+          start match {
+            case None => new Linear_Set[A](Some(elem), Some(elem), Map(), Map())
             case Some(elem1) =>
-              Linear_Set.make(Some(elem), rep.end,
-                rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
+              new Linear_Set[A](Some(elem), end,
+                nexts + (elem -> elem1), prevs + (elem1 -> elem))
           }
         case Some(elem1) =>
           if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
           else
-            rep.nexts.get(elem1) match {
+            nexts.get(elem1) match {
               case None =>
-                Linear_Set.make(rep.start, Some(elem),
-                  rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
+                new Linear_Set[A](start, Some(elem),
+                  nexts + (elem1 -> elem), prevs + (elem -> elem1))
               case Some(elem2) =>
-                Linear_Set.make(rep.start, rep.end,
-                  rep.nexts + (elem1 -> elem) + (elem -> elem2),
-                  rep.prevs + (elem2 -> elem) + (elem -> elem1))
+                new Linear_Set[A](start, end,
+                  nexts + (elem1 -> elem) + (elem -> elem2),
+                  prevs + (elem2 -> elem) + (elem -> elem1))
             }
       }
 
   def delete_after(hook: Option[A]): Linear_Set[A] =
     hook match {
       case None =>
-        rep.start match {
+        start match {
           case None => throw new Linear_Set.Next_Undefined[A](None)
           case Some(elem1) =>
-            rep.nexts.get(elem1) match {
+            nexts.get(elem1) match {
               case None => empty
               case Some(elem2) =>
-                Linear_Set.make(Some(elem2), rep.end, rep.nexts - elem1, rep.prevs - elem2)
+                new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2)
             }
         }
       case Some(elem1) =>
         if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
         else
-          rep.nexts.get(elem1) match {
+          nexts.get(elem1) match {
             case None => throw new Linear_Set.Next_Undefined(Some(elem1))
             case Some(elem2) =>
-              rep.nexts.get(elem2) match {
+              nexts.get(elem2) match {
                 case None =>
-                  Linear_Set.make(rep.start, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
+                  new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2)
                 case Some(elem3) =>
-                  Linear_Set.make(rep.start, rep.end,
-                    rep.nexts - elem2 + (elem1 -> elem3),
-                    rep.prevs - elem2 + (elem3 -> elem1))
+                  new Linear_Set[A](start, end,
+                    nexts - elem2 + (elem1 -> elem3),
+                    prevs - elem2 + (elem3 -> elem1))
               }
           }
     }
@@ -122,9 +112,9 @@
     if (isEmpty) this
     else {
       val next =
-        if (from == rep.end) None
-        else if (from == None) rep.start
-        else from.map(rep.nexts(_))
+        if (from == end) None
+        else if (from == None) start
+        else from.map(nexts(_))
       if (next == to) this
       else delete_after(from).delete_between(from, to)
     }
@@ -135,14 +125,14 @@
 
   override def stringPrefix = "Linear_Set"
 
-  override def isEmpty: Boolean = !rep.start.isDefined
-  override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
+  override def isEmpty: Boolean = !start.isDefined
+  override def size: Int = if (isEmpty) 0 else nexts.size + 1
 
   def contains(elem: A): Boolean =
-    !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
+    !isEmpty && (end.get == elem || nexts.isDefinedAt(elem))
 
-  private def make_iterator(start: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
-    private var next_elem = start
+  private def make_iterator(from: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
+    private var next_elem = from
     def hasNext(): Boolean = next_elem.isDefined
     def next(): A =
       next_elem match {
@@ -153,17 +143,17 @@
       }
   }
 
-  override def iterator: Iterator[A] = make_iterator(rep.start, rep.nexts)
+  override def iterator: Iterator[A] = make_iterator(start, nexts)
 
   def iterator(elem: A): Iterator[A] =
-    if (contains(elem)) make_iterator(Some(elem), rep.nexts)
+    if (contains(elem)) make_iterator(Some(elem), nexts)
     else throw new Linear_Set.Undefined(elem)
 
   def reverse_iterator(elem: A): Iterator[A] =
-    if (contains(elem)) make_iterator(Some(elem), rep.prevs)
+    if (contains(elem)) make_iterator(Some(elem), prevs)
     else throw new Linear_Set.Undefined(elem)
 
-  def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
+  def + (elem: A): Linear_Set[A] = insert_after(end, elem)
 
   def - (elem: A): Linear_Set[A] =
     if (!contains(elem)) throw new Linear_Set.Undefined(elem)
diff -r 2c5c003cee35 -r 5949ad86dc9a src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Thu Feb 23 20:33:35 2012 +0100
+++ b/src/Pure/General/scan.scala	Thu Feb 23 21:39:11 2012 +0100
@@ -7,8 +7,7 @@
 package isabelle
 
 
-import scala.collection.generic.Addable
-import scala.collection.IndexedSeq
+import scala.collection.{IndexedSeq, TraversableOnce}
 import scala.collection.immutable.PagedSeq
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
 import scala.util.parsing.combinator.RegexParsers
@@ -41,8 +40,7 @@
     def apply(elems: String*): Lexicon = empty ++ elems
   }
 
-  class Lexicon private(private val main_tree: Lexicon.Tree)
-    extends Addable[String, Lexicon] with RegexParsers
+  class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
   {
     import Lexicon.Tree
 
@@ -93,9 +91,7 @@
       }
 
 
-    /* Addable methods */
-
-    def repr = this
+    /* add elements */
 
     def + (elem: String): Lexicon =
       if (contains(elem)) this
@@ -115,10 +111,11 @@
             }
           }
           else tree
-        val old = this
-        new Lexicon(extend(old.main_tree, 0))
+        new Lexicon(extend(main_tree, 0))
       }
 
+    def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
+
 
 
     /** RegexParsers methods **/
diff -r 2c5c003cee35 -r 5949ad86dc9a src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Thu Feb 23 20:33:35 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Feb 23 21:39:11 2012 +0100
@@ -33,29 +33,22 @@
     result += '"'
     result.toString
   }
+
+  def init(): Outer_Syntax = new Outer_Syntax()
 }
 
-class Outer_Syntax
+class Outer_Syntax private(
+  keywords: Map[String, String] = Map((";" -> Keyword.DIAG)),
+  lexicon: Scan.Lexicon = Scan.Lexicon.empty,
+  val completion: Completion = Completion.init())
 {
-  protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
-  protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
-  lazy val completion: Completion = (new Completion).add_symbols // FIXME odd initialization
-
   def keyword_kind(name: String): Option[String] = keywords.get(name)
 
   def + (name: String, kind: String, replace: String): Outer_Syntax =
-  {
-    val new_keywords = keywords + (name -> kind)
-    val new_lexicon = lexicon + name
-    val new_completion =
-      if (Keyword.control(kind)) completion
-      else completion + (name, replace)
-    new Outer_Syntax {
-      override val lexicon = new_lexicon
-      override val keywords = new_keywords
-      override lazy val completion = new_completion
-    }
-  }
+    new Outer_Syntax(
+      keywords + (name -> kind),
+      lexicon + name,
+      if (Keyword.control(kind)) completion else completion + (name, replace))
 
   def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
 
diff -r 2c5c003cee35 -r 5949ad86dc9a src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Feb 23 20:33:35 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Feb 23 21:39:11 2012 +0100
@@ -116,7 +116,7 @@
 
   @volatile var verbose: Boolean = false
 
-  @volatile private var syntax = new Outer_Syntax
+  @volatile private var syntax = Outer_Syntax.init()
   def current_syntax(): Outer_Syntax = syntax
 
   @volatile private var reverse_syslog = List[XML.Elem]()
diff -r 2c5c003cee35 -r 5949ad86dc9a src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Thu Feb 23 20:33:35 2012 +0100
+++ b/src/Pure/Thy/completion.scala	Thu Feb 23 21:39:11 2012 +0100
@@ -10,14 +10,18 @@
 import scala.util.parsing.combinator.RegexParsers
 
 
-private object Completion
+object Completion
 {
+  val empty: Completion = new Completion()
+  def init(): Completion = empty.add_symbols()
+
+
   /** word completion **/
 
-  val word_regex = "[a-zA-Z0-9_']+".r
-  def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
+  private val word_regex = "[a-zA-Z0-9_']+".r
+  private def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
 
-  object Parse extends RegexParsers
+  private object Parse extends RegexParsers
   {
     override val whiteSpace = "".r
 
@@ -36,33 +40,24 @@
   }
 }
 
-class Completion
+class Completion private(
+  words_lex: Scan.Lexicon = Scan.Lexicon.empty,
+  words_map: Map[String, String] = Map.empty,
+  abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
+  abbrevs_map: Map[String, (String, String)] = Map.empty)
 {
-  /* representation */
-
-  protected val words_lex = Scan.Lexicon()
-  protected val words_map = Map[String, String]()
-
-  protected val abbrevs_lex = Scan.Lexicon()
-  protected val abbrevs_map = Map[String, (String, String)]()
-
-
   /* adding stuff */
 
   def + (keyword: String, replace: String): Completion =
-  {
-    val old = this
-    new Completion {
-      override val words_lex = old.words_lex + keyword
-      override val words_map = old.words_map + (keyword -> replace)
-      override val abbrevs_lex = old.abbrevs_lex
-      override val abbrevs_map = old.abbrevs_map
-    }
-  }
+    new Completion(
+      words_lex + keyword,
+      words_map + (keyword -> replace),
+      abbrevs_lex,
+      abbrevs_map)
 
   def + (keyword: String): Completion = this + (keyword, keyword)
 
-  def add_symbols: Completion =
+  private def add_symbols(): Completion =
   {
     val words =
       (for ((x, _) <- Symbol.names) yield (x, x)).toList :::
@@ -73,13 +68,11 @@
       (for ((x, y) <- Symbol.abbrevs if !Completion.is_word(y))
         yield (y.reverse.toString, (y, x))).toList
 
-    val old = this
-    new Completion {
-      override val words_lex = old.words_lex ++ words.map(_._1)
-      override val words_map = old.words_map ++ words
-      override val abbrevs_lex = old.abbrevs_lex ++ abbrs.map(_._1)
-      override val abbrevs_map = old.abbrevs_map ++ abbrs
-    }
+    new Completion(
+      words_lex ++ words.map(_._1),
+      words_map ++ words,
+      abbrevs_lex ++ abbrs.map(_._1),
+      abbrevs_map ++ abbrs)
   }