# HG changeset patch
# User wenzelm
# Date 1482220406 -3600
# Node ID 1b89608974e9c569fd73fc1a738fc69395e91a2b
# Parent  7cc4b49be1ea25d611fa36ef6f1eabc656f9fdc6
clarified modules;

diff -r 7cc4b49be1ea -r 1b89608974e9 src/Pure/Admin/check_sources.scala
--- a/src/Pure/Admin/check_sources.scala	Tue Dec 20 08:46:38 2016 +0100
+++ b/src/Pure/Admin/check_sources.scala	Tue Dec 20 08:53:26 2016 +0100
@@ -25,9 +25,9 @@
       try {
         Symbol.decode_strict(line)
 
-        for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
+        for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) }
         {
-          Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
+          Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) +
             Position.here(line_pos(i)))
         }
       }
diff -r 7cc4b49be1ea -r 1b89608974e9 src/Pure/General/codepoint.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/codepoint.scala	Tue Dec 20 08:53:26 2016 +0100
@@ -0,0 +1,25 @@
+/*  Title:      Pure/General/codepoint.scala
+    Author:     Makarius
+
+Unicode codepoints vs. Unicode string encoding.
+*/
+
+package isabelle
+
+
+object Codepoint
+{
+  def iterator(str: String): Iterator[Int] =
+    new Iterator[Int] {
+      var offset = 0
+      def hasNext: Boolean = offset < str.length
+      def next: Int =
+      {
+        val c = str.codePointAt(offset)
+        offset += Character.charCount(c)
+        c
+      }
+    }
+
+  def string(c: Int): String = new String(Array(c), 0, 1)
+}
diff -r 7cc4b49be1ea -r 1b89608974e9 src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Tue Dec 20 08:46:38 2016 +0100
+++ b/src/Pure/General/word.scala	Tue Dec 20 08:53:26 2016 +0100
@@ -12,23 +12,6 @@
 
 object Word
 {
-  /* codepoints */
-
-  def codepoint_iterator(str: String): Iterator[Int] =
-    new Iterator[Int] {
-      var offset = 0
-      def hasNext: Boolean = offset < str.length
-      def next: Int =
-      {
-        val c = str.codePointAt(offset)
-        offset += Character.charCount(c)
-        c
-      }
-    }
-
-  def codepoint(c: Int): String = new String(Array(c), 0, 1)
-
-
   /* directionality */
 
   def bidi_detect(str: String): Boolean =
@@ -51,7 +34,7 @@
     }
 
   def perhaps_capitalize(str: String): String =
-    if (codepoint_iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
+    if (Codepoint.iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
       capitalize(str)
     else str
 
@@ -70,10 +53,10 @@
       }
     def unapply(str: String): Option[Case] =
       if (str.nonEmpty) {
-        if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
-        else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
+        if (Codepoint.iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
+        else if (Codepoint.iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
         else {
-          val it = codepoint_iterator(str)
+          val it = Codepoint.iterator(str)
           if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_)))
             Some(Capitalized)
           else None
diff -r 7cc4b49be1ea -r 1b89608974e9 src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala	Tue Dec 20 08:46:38 2016 +0100
+++ b/src/Pure/Isar/document_structure.scala	Tue Dec 20 08:53:26 2016 +0100
@@ -190,8 +190,7 @@
         toks.filterNot(_.is_space) match {
           case List(tok) if tok.is_comment =>
             val s = tok.source
-            if (Word.codepoint_iterator(s).exists(c =>
-                  Character.isLetter(c) || Character.isDigit(c)))
+            if (Codepoint.iterator(s).exists(c => Character.isLetter(c) || Character.isDigit(c)))
             {
               if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
               else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
diff -r 7cc4b49be1ea -r 1b89608974e9 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Dec 20 08:46:38 2016 +0100
+++ b/src/Pure/build-jars	Tue Dec 20 08:53:26 2016 +0100
@@ -39,6 +39,7 @@
   GUI/wrap_panel.scala
   General/antiquote.scala
   General/bytes.scala
+  General/codepoint.scala
   General/completion.scala
   General/date.scala
   General/exn.scala
diff -r 7cc4b49be1ea -r 1b89608974e9 src/Tools/VSCode/src/line.scala
--- a/src/Tools/VSCode/src/line.scala	Tue Dec 20 08:46:38 2016 +0100
+++ b/src/Tools/VSCode/src/line.scala	Tue Dec 20 08:53:26 2016 +0100
@@ -50,7 +50,7 @@
       if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _)
 
     def advance_codepoints(text: String): Position =
-      if (text.isEmpty) this else advance[Int](Word.codepoint_iterator(text), _ == 10)
+      if (text.isEmpty) this else advance[Int](Codepoint.iterator(text), _ == 10)
   }
 
 
@@ -139,7 +139,7 @@
   require(text.forall(c => c != '\r' && c != '\n'))
 
   lazy val length_symbols: Int = Symbol.iterator(text).length
-  lazy val length_codepoints: Int = Word.codepoint_iterator(text).length
+  lazy val length_codepoints: Int = Codepoint.iterator(text).length
 
   override def equals(that: Any): Boolean =
     that match {