src/Pure/PIDE/command.scala
changeset 59735 24bee1b11fce
parent 59715 4f0d0e4ad68d
child 59924 801b979ec0c2
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Mar 17 09:22:21 2015 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Mar 17 15:21:41 2015 +0100
     1.3 @@ -235,7 +235,7 @@
     1.4                  for {
     1.5                    (chunk_name, chunk) <- command.chunks.iterator
     1.6                    range <- Protocol_Message.positions(
     1.7 -                    self_id, command.position, chunk_name, chunk, message)
     1.8 +                    self_id, command.span.position, chunk_name, chunk, message)
     1.9                  } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
    1.10                }
    1.11                st
    1.12 @@ -334,19 +334,15 @@
    1.13      }
    1.14  
    1.15    def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
    1.16 -    span.kind match {
    1.17 -      case Command_Span.Command_Span(name, _) =>
    1.18 -        syntax.load_command(name) match {
    1.19 -          case Some(exts) =>
    1.20 -            find_file(clean_tokens(span.content)) match {
    1.21 -              case Some((file, i)) =>
    1.22 -                if (exts.isEmpty) (List(file), i)
    1.23 -                else (exts.map(ext => file + "." + ext), i)
    1.24 -              case None => (Nil, -1)
    1.25 -            }
    1.26 +    syntax.load_command(span.name) match {
    1.27 +      case Some(exts) =>
    1.28 +        find_file(clean_tokens(span.content)) match {
    1.29 +          case Some((file, i)) =>
    1.30 +            if (exts.isEmpty) (List(file), i)
    1.31 +            else (exts.map(ext => file + "." + ext), i)
    1.32            case None => (Nil, -1)
    1.33          }
    1.34 -      case _ => (Nil, -1)
    1.35 +      case None => (Nil, -1)
    1.36      }
    1.37  
    1.38    def blobs_info(
    1.39 @@ -357,12 +353,12 @@
    1.40      node_name: Document.Node.Name,
    1.41      span: Command_Span.Span): Blobs_Info =
    1.42    {
    1.43 -    span.kind match {
    1.44 +    span.name match {
    1.45        // inlined errors
    1.46 -      case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
    1.47 +      case Thy_Header.THEORY =>
    1.48          val header =
    1.49            resources.check_thy_reader("", node_name,
    1.50 -            new CharSequenceReader(span.source), Token.Pos.command)
    1.51 +            new CharSequenceReader(Token.implode(span.content)), Token.Pos.command)
    1.52          val errors =
    1.53            for ((imp, pos) <- header.imports if !can_import(imp)) yield {
    1.54              val msg =
    1.55 @@ -398,14 +394,6 @@
    1.56      val init_results: Command.Results,
    1.57      val init_markup: Markup_Tree)
    1.58  {
    1.59 -  /* name */
    1.60 -
    1.61 -  def name: String =
    1.62 -    span.kind match { case Command_Span.Command_Span(name, _) => name case _ => "" }
    1.63 -
    1.64 -  def position: Position.T =
    1.65 -    span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none }
    1.66 -
    1.67    override def toString: String = id + "/" + span.kind.toString
    1.68  
    1.69