--- 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} +) ')'
--- 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}}
--- 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
--- 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]]
}
--- 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)
--- 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 **/
--- 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)
--- 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]()
--- 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)
}