src/Pure/PIDE/command.scala
changeset 56746 d37a5d09a277
parent 56743 81370dfadb1d
child 56782 433cf57550fa
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Apr 26 13:32:28 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Apr 26 13:34:10 2014 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  object Command
     1.5  {
     1.6    type Edit = (Option[Command], Option[Command])
     1.7 -  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk)])]
     1.8 +  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])]
     1.9  
    1.10  
    1.11  
    1.12 @@ -60,10 +60,10 @@
    1.13  
    1.14    object Markup_Index
    1.15    {
    1.16 -    val markup: Markup_Index = Markup_Index(false, Text.Chunk.Default)
    1.17 +    val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default)
    1.18    }
    1.19  
    1.20 -  sealed case class Markup_Index(status: Boolean, chunk_name: Text.Chunk.Name)
    1.21 +  sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name)
    1.22  
    1.23    object Markups
    1.24    {
    1.25 @@ -84,16 +84,16 @@
    1.26        new Markups(rep + (index -> (this(index) + markup)))
    1.27  
    1.28      def redirection_iterator: Iterator[Document_ID.Generic] =
    1.29 -      for (Markup_Index(_, Text.Chunk.Id(id)) <- rep.keysIterator)
    1.30 +      for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
    1.31          yield id
    1.32  
    1.33      def redirect(other_id: Document_ID.Generic): Markups =
    1.34      {
    1.35        val rep1 =
    1.36          (for {
    1.37 -          (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
    1.38 +          (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator
    1.39            if other_id == id
    1.40 -        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap
    1.41 +        } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap
    1.42        if (rep1.isEmpty) Markups.empty else new Markups(rep1)
    1.43      }
    1.44  
    1.45 @@ -156,7 +156,8 @@
    1.46      private def add_status(st: Markup): State =
    1.47        copy(status = st :: status)
    1.48  
    1.49 -    private def add_markup(status: Boolean, chunk_name: Text.Chunk.Name, m: Text.Markup): State =
    1.50 +    private def add_markup(
    1.51 +      status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
    1.52      {
    1.53        val markups1 =
    1.54          if (status || Protocol.liberal_status_elements(m.info.name))
    1.55 @@ -167,7 +168,7 @@
    1.56  
    1.57      def accumulate(
    1.58          self_id: Document_ID.Generic => Boolean,
    1.59 -        other_id: Document_ID.Generic => Option[(Text.Chunk.Id, Text.Chunk)],
    1.60 +        other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
    1.61          message: XML.Elem): State =
    1.62        message match {
    1.63          case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    1.64 @@ -176,7 +177,7 @@
    1.65                case elem @ XML.Elem(markup, Nil) =>
    1.66                  state.
    1.67                    add_status(markup).
    1.68 -                  add_markup(true, Text.Chunk.Default, Text.Info(command.proper_range, elem))
    1.69 +                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
    1.70                case _ =>
    1.71                  System.err.println("Ignored status message: " + msg)
    1.72                  state
    1.73 @@ -194,7 +195,7 @@
    1.74                    val target =
    1.75                      if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
    1.76                        Some((chunk_name, command.chunks(chunk_name)))
    1.77 -                    else if (chunk_name == Text.Chunk.Default) other_id(id)
    1.78 +                    else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
    1.79                      else None
    1.80  
    1.81                    target match {
    1.82 @@ -216,7 +217,7 @@
    1.83                    val range = command.proper_range
    1.84                    val props = Position.purge(atts)
    1.85                    val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.86 -                  state.add_markup(false, Text.Chunk.Default, info)
    1.87 +                  state.add_markup(false, Symbol.Text_Chunk.Default, info)
    1.88  
    1.89                  case _ => bad(); state
    1.90                }
    1.91 @@ -365,12 +366,12 @@
    1.92  
    1.93    /* source chunks */
    1.94  
    1.95 -  val chunk: Text.Chunk = Text.Chunk(source)
    1.96 +  val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source)
    1.97  
    1.98 -  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
    1.99 -    ((Text.Chunk.Default -> chunk) ::
   1.100 +  val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
   1.101 +    ((Symbol.Text_Chunk.Default -> chunk) ::
   1.102        (for (Exn.Res((name, Some((_, file)))) <- blobs)
   1.103 -        yield (Text.Chunk.File(name.node) -> file))).toMap
   1.104 +        yield (Symbol.Text_Chunk.File(name.node) -> file))).toMap
   1.105  
   1.106    def length: Int = source.length
   1.107    def range: Text.Range = chunk.range