clarified modules;
authorwenzelm
Tue Dec 20 08:53:26 2016 +0100 (2016-12-20)
changeset 646101b89608974e9
parent 64609 7cc4b49be1ea
child 64611 d72d63d05bdb
clarified modules;
src/Pure/Admin/check_sources.scala
src/Pure/General/codepoint.scala
src/Pure/General/word.scala
src/Pure/Isar/document_structure.scala
src/Pure/build-jars
src/Tools/VSCode/src/line.scala
     1.1 --- a/src/Pure/Admin/check_sources.scala	Tue Dec 20 08:46:38 2016 +0100
     1.2 +++ b/src/Pure/Admin/check_sources.scala	Tue Dec 20 08:53:26 2016 +0100
     1.3 @@ -25,9 +25,9 @@
     1.4        try {
     1.5          Symbol.decode_strict(line)
     1.6  
     1.7 -        for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
     1.8 +        for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) }
     1.9          {
    1.10 -          Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
    1.11 +          Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) +
    1.12              Position.here(line_pos(i)))
    1.13          }
    1.14        }
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/codepoint.scala	Tue Dec 20 08:53:26 2016 +0100
     2.3 @@ -0,0 +1,25 @@
     2.4 +/*  Title:      Pure/General/codepoint.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Unicode codepoints vs. Unicode string encoding.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Codepoint
    2.14 +{
    2.15 +  def iterator(str: String): Iterator[Int] =
    2.16 +    new Iterator[Int] {
    2.17 +      var offset = 0
    2.18 +      def hasNext: Boolean = offset < str.length
    2.19 +      def next: Int =
    2.20 +      {
    2.21 +        val c = str.codePointAt(offset)
    2.22 +        offset += Character.charCount(c)
    2.23 +        c
    2.24 +      }
    2.25 +    }
    2.26 +
    2.27 +  def string(c: Int): String = new String(Array(c), 0, 1)
    2.28 +}
     3.1 --- a/src/Pure/General/word.scala	Tue Dec 20 08:46:38 2016 +0100
     3.2 +++ b/src/Pure/General/word.scala	Tue Dec 20 08:53:26 2016 +0100
     3.3 @@ -12,23 +12,6 @@
     3.4  
     3.5  object Word
     3.6  {
     3.7 -  /* codepoints */
     3.8 -
     3.9 -  def codepoint_iterator(str: String): Iterator[Int] =
    3.10 -    new Iterator[Int] {
    3.11 -      var offset = 0
    3.12 -      def hasNext: Boolean = offset < str.length
    3.13 -      def next: Int =
    3.14 -      {
    3.15 -        val c = str.codePointAt(offset)
    3.16 -        offset += Character.charCount(c)
    3.17 -        c
    3.18 -      }
    3.19 -    }
    3.20 -
    3.21 -  def codepoint(c: Int): String = new String(Array(c), 0, 1)
    3.22 -
    3.23 -
    3.24    /* directionality */
    3.25  
    3.26    def bidi_detect(str: String): Boolean =
    3.27 @@ -51,7 +34,7 @@
    3.28      }
    3.29  
    3.30    def perhaps_capitalize(str: String): String =
    3.31 -    if (codepoint_iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
    3.32 +    if (Codepoint.iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
    3.33        capitalize(str)
    3.34      else str
    3.35  
    3.36 @@ -70,10 +53,10 @@
    3.37        }
    3.38      def unapply(str: String): Option[Case] =
    3.39        if (str.nonEmpty) {
    3.40 -        if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
    3.41 -        else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
    3.42 +        if (Codepoint.iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
    3.43 +        else if (Codepoint.iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
    3.44          else {
    3.45 -          val it = codepoint_iterator(str)
    3.46 +          val it = Codepoint.iterator(str)
    3.47            if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_)))
    3.48              Some(Capitalized)
    3.49            else None
     4.1 --- a/src/Pure/Isar/document_structure.scala	Tue Dec 20 08:46:38 2016 +0100
     4.2 +++ b/src/Pure/Isar/document_structure.scala	Tue Dec 20 08:53:26 2016 +0100
     4.3 @@ -190,8 +190,7 @@
     4.4          toks.filterNot(_.is_space) match {
     4.5            case List(tok) if tok.is_comment =>
     4.6              val s = tok.source
     4.7 -            if (Word.codepoint_iterator(s).exists(c =>
     4.8 -                  Character.isLetter(c) || Character.isDigit(c)))
     4.9 +            if (Codepoint.iterator(s).exists(c => Character.isLetter(c) || Character.isDigit(c)))
    4.10              {
    4.11                if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
    4.12                else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
     5.1 --- a/src/Pure/build-jars	Tue Dec 20 08:46:38 2016 +0100
     5.2 +++ b/src/Pure/build-jars	Tue Dec 20 08:53:26 2016 +0100
     5.3 @@ -39,6 +39,7 @@
     5.4    GUI/wrap_panel.scala
     5.5    General/antiquote.scala
     5.6    General/bytes.scala
     5.7 +  General/codepoint.scala
     5.8    General/completion.scala
     5.9    General/date.scala
    5.10    General/exn.scala
     6.1 --- a/src/Tools/VSCode/src/line.scala	Tue Dec 20 08:46:38 2016 +0100
     6.2 +++ b/src/Tools/VSCode/src/line.scala	Tue Dec 20 08:53:26 2016 +0100
     6.3 @@ -50,7 +50,7 @@
     6.4        if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _)
     6.5  
     6.6      def advance_codepoints(text: String): Position =
     6.7 -      if (text.isEmpty) this else advance[Int](Word.codepoint_iterator(text), _ == 10)
     6.8 +      if (text.isEmpty) this else advance[Int](Codepoint.iterator(text), _ == 10)
     6.9    }
    6.10  
    6.11  
    6.12 @@ -139,7 +139,7 @@
    6.13    require(text.forall(c => c != '\r' && c != '\n'))
    6.14  
    6.15    lazy val length_symbols: Int = Symbol.iterator(text).length
    6.16 -  lazy val length_codepoints: Int = Word.codepoint_iterator(text).length
    6.17 +  lazy val length_codepoints: Int = Codepoint.iterator(text).length
    6.18  
    6.19    override def equals(that: Any): Boolean =
    6.20      that match {