misc tuning and simplification;
authorwenzelm
Tue Mar 17 15:21:41 2015 +0100 (2015-03-17)
changeset 5973524bee1b11fce
parent 59729 ba54b27d733d
child 59736 5c1a0069b9d3
misc tuning and simplification;
src/Pure/Isar/keyword.ML
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/token.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/command_span.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/prover.scala
src/Pure/Thy/thy_header.ML
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Pure/Isar/keyword.ML	Tue Mar 17 09:22:21 2015 +0100
     1.2 +++ b/src/Pure/Isar/keyword.ML	Tue Mar 17 15:21:41 2015 +0100
     1.3 @@ -50,7 +50,6 @@
     1.4    val is_document_body: keywords -> string -> bool
     1.5    val is_document_raw: keywords -> string -> bool
     1.6    val is_document: keywords -> string -> bool
     1.7 -  val is_theory_begin: keywords -> string -> bool
     1.8    val is_theory_end: keywords -> string -> bool
     1.9    val is_theory_load: keywords -> string -> bool
    1.10    val is_theory: keywords -> string -> bool
    1.11 @@ -219,7 +218,6 @@
    1.12  val is_document_raw = command_category [document_raw];
    1.13  val is_document = command_category [document_heading, document_body, document_raw];
    1.14  
    1.15 -val is_theory_begin = command_category [thy_begin];
    1.16  val is_theory_end = command_category [thy_end];
    1.17  
    1.18  val is_theory_load = command_category [thy_load];
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Mar 17 09:22:21 2015 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Mar 17 15:21:41 2015 +0100
     2.3 @@ -123,9 +123,7 @@
     2.4      }
     2.5  
     2.6  
     2.7 -  /* command categories */
     2.8 -
     2.9 -  def is_theory_begin(name: String): Boolean = keywords.is_command_kind(name, Keyword.theory_begin)
    2.10 +  /* load commands */
    2.11  
    2.12    def load_command(name: String): Option[List[String]] = keywords.load_command(name)
    2.13    def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
    2.14 @@ -230,13 +228,14 @@
    2.15  
    2.16    def heading_level(command: Command): Option[Int] =
    2.17    {
    2.18 -    command.name match {
    2.19 -      case "chapter" => Some(0)
    2.20 -      case "section" | "header" => Some(1)
    2.21 -      case "subsection" => Some(2)
    2.22 -      case "subsubsection" => Some(3)
    2.23 +    val name = command.span.name
    2.24 +    name match {
    2.25 +      case Thy_Header.CHAPTER => Some(0)
    2.26 +      case Thy_Header.SECTION | Thy_Header.HEADER => Some(1)
    2.27 +      case Thy_Header.SUBSECTION => Some(2)
    2.28 +      case Thy_Header.SUBSUBSECTION => Some(3)
    2.29        case _ =>
    2.30 -        keywords.command_kind(command.name) match {
    2.31 +        keywords.command_kind(name) match {
    2.32            case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
    2.33            case _ => None
    2.34          }
    2.35 @@ -258,7 +257,7 @@
    2.36      {
    2.37        stack match {
    2.38          case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
    2.39 -          body2 += Outer_Syntax.Document_Block(command.name, command.source, body.toList)
    2.40 +          body2 += Outer_Syntax.Document_Block(command.span.name, command.source, body.toList)
    2.41            stack = stack.tail
    2.42            close(level)
    2.43          case _ =>
     3.1 --- a/src/Pure/Isar/token.scala	Tue Mar 17 09:22:21 2015 +0100
     3.2 +++ b/src/Pure/Isar/token.scala	Tue Mar 17 15:21:41 2015 +0100
     3.3 @@ -153,6 +153,15 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* implode */
     3.8 +
     3.9 +  def implode(toks: List[Token]): String =
    3.10 +    toks match {
    3.11 +      case List(tok) => tok.source
    3.12 +      case toks => toks.map(_.source).mkString
    3.13 +    }
    3.14 +
    3.15 +
    3.16    /* token reader */
    3.17  
    3.18    object Pos
     4.1 --- a/src/Pure/PIDE/command.scala	Tue Mar 17 09:22:21 2015 +0100
     4.2 +++ b/src/Pure/PIDE/command.scala	Tue Mar 17 15:21:41 2015 +0100
     4.3 @@ -235,7 +235,7 @@
     4.4                  for {
     4.5                    (chunk_name, chunk) <- command.chunks.iterator
     4.6                    range <- Protocol_Message.positions(
     4.7 -                    self_id, command.position, chunk_name, chunk, message)
     4.8 +                    self_id, command.span.position, chunk_name, chunk, message)
     4.9                  } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
    4.10                }
    4.11                st
    4.12 @@ -334,19 +334,15 @@
    4.13      }
    4.14  
    4.15    def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
    4.16 -    span.kind match {
    4.17 -      case Command_Span.Command_Span(name, _) =>
    4.18 -        syntax.load_command(name) match {
    4.19 -          case Some(exts) =>
    4.20 -            find_file(clean_tokens(span.content)) match {
    4.21 -              case Some((file, i)) =>
    4.22 -                if (exts.isEmpty) (List(file), i)
    4.23 -                else (exts.map(ext => file + "." + ext), i)
    4.24 -              case None => (Nil, -1)
    4.25 -            }
    4.26 +    syntax.load_command(span.name) match {
    4.27 +      case Some(exts) =>
    4.28 +        find_file(clean_tokens(span.content)) match {
    4.29 +          case Some((file, i)) =>
    4.30 +            if (exts.isEmpty) (List(file), i)
    4.31 +            else (exts.map(ext => file + "." + ext), i)
    4.32            case None => (Nil, -1)
    4.33          }
    4.34 -      case _ => (Nil, -1)
    4.35 +      case None => (Nil, -1)
    4.36      }
    4.37  
    4.38    def blobs_info(
    4.39 @@ -357,12 +353,12 @@
    4.40      node_name: Document.Node.Name,
    4.41      span: Command_Span.Span): Blobs_Info =
    4.42    {
    4.43 -    span.kind match {
    4.44 +    span.name match {
    4.45        // inlined errors
    4.46 -      case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
    4.47 +      case Thy_Header.THEORY =>
    4.48          val header =
    4.49            resources.check_thy_reader("", node_name,
    4.50 -            new CharSequenceReader(span.source), Token.Pos.command)
    4.51 +            new CharSequenceReader(Token.implode(span.content)), Token.Pos.command)
    4.52          val errors =
    4.53            for ((imp, pos) <- header.imports if !can_import(imp)) yield {
    4.54              val msg =
    4.55 @@ -398,14 +394,6 @@
    4.56      val init_results: Command.Results,
    4.57      val init_markup: Markup_Tree)
    4.58  {
    4.59 -  /* name */
    4.60 -
    4.61 -  def name: String =
    4.62 -    span.kind match { case Command_Span.Command_Span(name, _) => name case _ => "" }
    4.63 -
    4.64 -  def position: Position.T =
    4.65 -    span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none }
    4.66 -
    4.67    override def toString: String = id + "/" + span.kind.toString
    4.68  
    4.69  
     5.1 --- a/src/Pure/PIDE/command_span.scala	Tue Mar 17 09:22:21 2015 +0100
     5.2 +++ b/src/Pure/PIDE/command_span.scala	Tue Mar 17 15:21:41 2015 +0100
     5.3 @@ -26,26 +26,26 @@
     5.4  
     5.5    sealed case class Span(kind: Kind, content: List[Token])
     5.6    {
     5.7 -    def length: Int = (0 /: content)(_ + _.source.length)
     5.8 +    def name: String =
     5.9 +      kind match { case Command_Span(name, _) => name case _ => "" }
    5.10  
    5.11 -    def source: String =
    5.12 -      content match {
    5.13 -        case List(tok) => tok.source
    5.14 -        case toks => toks.map(_.source).mkString
    5.15 -      }
    5.16 +    def position: Position.T =
    5.17 +      kind match { case Command_Span(_, pos) => pos case _ => Position.none }
    5.18 +
    5.19 +    def length: Int = (0 /: content)(_ + _.source.length)
    5.20  
    5.21      def compact_source: (String, Span) =
    5.22      {
    5.23 -      val src = source
    5.24 +      val source = Token.implode(content)
    5.25        val content1 = new mutable.ListBuffer[Token]
    5.26        var i = 0
    5.27        for (Token(kind, s) <- content) {
    5.28          val n = s.length
    5.29 -        val s1 = src.substring(i, i + n)
    5.30 +        val s1 = source.substring(i, i + n)
    5.31          content1 += Token(kind, s1)
    5.32          i += n
    5.33        }
    5.34 -      (src, Span(kind, content1.toList))
    5.35 +      (source, Span(kind, content1.toList))
    5.36      }
    5.37    }
    5.38  
     6.1 --- a/src/Pure/PIDE/document.ML	Tue Mar 17 09:22:21 2015 +0100
     6.2 +++ b/src/Pure/PIDE/document.ML	Tue Mar 17 15:21:41 2015 +0100
     6.3 @@ -552,8 +552,7 @@
     6.4          val initial' = initial andalso
     6.5            (case prev of
     6.6              NONE => true
     6.7 -          | SOME command_id =>
     6.8 -              not (Keyword.is_theory_begin keywords (the_command_name state command_id)));
     6.9 +          | SOME command_id => the_command_name state command_id <> Thy_Header.theoryN);
    6.10        in (visible', initial') end;
    6.11  
    6.12      fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
    6.13 @@ -614,7 +613,7 @@
    6.14        val exec' = (eval', prints');
    6.15  
    6.16        val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    6.17 -      val init' = if Keyword.is_theory_begin keywords command_name then NONE else init;
    6.18 +      val init' = if command_name = Thy_Header.theoryN then NONE else init;
    6.19      in SOME (assign_update', (command_id', (eval', prints')), init') end;
    6.20  
    6.21  fun removed_execs node0 (command_id, exec_ids) =
     7.1 --- a/src/Pure/PIDE/protocol.scala	Tue Mar 17 09:22:21 2015 +0100
     7.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Mar 17 15:21:41 2015 +0100
     7.3 @@ -329,7 +329,7 @@
     7.4      }
     7.5  
     7.6      protocol_command("Document.define_command",
     7.7 -      (Document_ID(command.id) :: encode(command.name) :: blobs_yxml :: toks_yxml ::
     7.8 +      (Document_ID(command.id) :: encode(command.span.name) :: blobs_yxml :: toks_yxml ::
     7.9          toks.map(tok => encode(tok.source))): _*)
    7.10    }
    7.11  
     8.1 --- a/src/Pure/PIDE/prover.scala	Tue Mar 17 09:22:21 2015 +0100
     8.2 +++ b/src/Pure/PIDE/prover.scala	Tue Mar 17 15:21:41 2015 +0100
     8.3 @@ -20,7 +20,6 @@
     8.4      def ++ (other: Syntax): Syntax
     8.5      def add_keywords(keywords: Thy_Header.Keywords): Syntax
     8.6      def parse_spans(input: CharSequence): List[Command_Span.Span]
     8.7 -    def is_theory_begin(name: String): Boolean
     8.8      def load_command(name: String): Option[List[String]]
     8.9      def load_commands_in(text: String): Boolean
    8.10    }
     9.1 --- a/src/Pure/Thy/thy_header.ML	Tue Mar 17 09:22:21 2015 +0100
     9.2 +++ b/src/Pure/Thy/thy_header.ML	Tue Mar 17 15:21:41 2015 +0100
     9.3 @@ -12,6 +12,7 @@
     9.4      imports: (string * Position.T) list,
     9.5      keywords: keywords}
     9.6    val make: string * Position.T -> (string * Position.T) list -> keywords -> header
     9.7 +  val theoryN: string
     9.8    val bootstrap_keywords: Keyword.keywords
     9.9    val add_keywords: keywords -> theory -> theory
    9.10    val get_keywords: theory -> Keyword.keywords
    10.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 17 09:22:21 2015 +0100
    10.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 17 15:21:41 2015 +0100
    10.3 @@ -86,13 +86,15 @@
    10.4    private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
    10.5      extends Entry
    10.6    {
    10.7 -    def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
    10.8 +    def print: String =
    10.9 +      Time.print_seconds(timing) + "s theory " + quote(name.theory)
   10.10      def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(view, name.node) }
   10.11    }
   10.12  
   10.13    private case class Command_Entry(command: Command, timing: Double) extends Entry
   10.14    {
   10.15 -    def print: String = "  " + Time.print_seconds(timing) + "s command " + quote(command.name)
   10.16 +    def print: String =
   10.17 +      "  " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
   10.18      def follow(snapshot: Document.Snapshot)
   10.19      { PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) }
   10.20    }