src/Pure/PIDE/command.scala
changeset 57905 c0c5652e796e
parent 57904 922273b7bf8a
child 57910 a50837b637dc
     1.1 --- a/src/Pure/PIDE/command.scala	Mon Aug 11 22:59:38 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 12 00:08:32 2014 +0200
     1.3 @@ -254,14 +254,14 @@
     1.4      id: Document_ID.Command,
     1.5      node_name: Document.Node.Name,
     1.6      blobs: List[Blob],
     1.7 -    span: Thy_Syntax.Span): Command =
     1.8 +    span: Command_Span.Span): Command =
     1.9    {
    1.10      val (source, span1) = span.compact_source
    1.11      new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
    1.12    }
    1.13  
    1.14    val empty: Command =
    1.15 -    Command(Document_ID.none, Document.Node.Name.empty, Nil, Thy_Syntax.empty_span)
    1.16 +    Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
    1.17  
    1.18    def unparsed(
    1.19      id: Document_ID.Command,
    1.20 @@ -269,7 +269,7 @@
    1.21      results: Results,
    1.22      markup: Markup_Tree): Command =
    1.23    {
    1.24 -    val (source1, span1) = Thy_Syntax.unparsed_span(source).compact_source
    1.25 +    val (source1, span1) = Command_Span.unparsed(source).compact_source
    1.26      new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
    1.27    }
    1.28  
    1.29 @@ -312,7 +312,7 @@
    1.30      val id: Document_ID.Command,
    1.31      val node_name: Document.Node.Name,
    1.32      val blobs: List[Command.Blob],
    1.33 -    val span: Thy_Syntax.Span,
    1.34 +    val span: Command_Span.Span,
    1.35      val source: String,
    1.36      val init_results: Command.Results,
    1.37      val init_markup: Markup_Tree)
    1.38 @@ -320,12 +320,12 @@
    1.39    /* name and classification */
    1.40  
    1.41    def name: String =
    1.42 -    span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" }
    1.43 +    span.kind match { case Command_Span.Command_Span(name) => name case _ => "" }
    1.44  
    1.45    override def toString = id + "/" + span.kind.toString
    1.46  
    1.47 -  def is_proper: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
    1.48 -  def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
    1.49 +  def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span]
    1.50 +  def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span
    1.51  
    1.52    def is_undefined: Boolean = id == Document_ID.none
    1.53    val is_unparsed: Boolean = span.content.exists(_.is_unparsed)