src/Pure/Thy/thy_syntax.scala
author wenzelm
Mon, 29 Aug 2011 21:55:49 +0200
changeset 44574 24444588fddd
parent 44474 681447a9ffe5
child 44607 274eff0ea12e
permissions -rw-r--r--
actual auto loading of required files; eliminated File_Store in favour of Thy_Load; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34268
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/thy_syntax.scala
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
     3
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
     4
Superficial theory syntax: tokens and spans.
34268
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
     5
*/
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
     6
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
     7
package isabelle
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
     8
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
     9
38239
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    10
import scala.collection.mutable
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
    11
import scala.annotation.tailrec
38239
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    12
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    13
34303
98425e77cfeb plain object;
wenzelm
parents: 34268
diff changeset
    14
object Thy_Syntax
34268
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
    15
{
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    16
  /** nested structure **/
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    17
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    18
  object Structure
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    19
  {
40478
4bae781b8f7c replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents: 40457
diff changeset
    20
    sealed abstract class Entry { def length: Int }
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    21
    case class Block(val name: String, val body: List[Entry]) extends Entry
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    22
    {
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    23
      val length: Int = (0 /: body)(_ + _.length)
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    24
    }
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    25
    case class Atom(val command: Command) extends Entry
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    26
    {
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    27
      def length: Int = command.length
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    28
    }
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    29
40792
1d71a45590e4 tuned signature;
wenzelm
parents: 40479
diff changeset
    30
    def parse(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    31
    {
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    32
      /* stack operations */
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    33
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    34
      def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    35
      var stack: List[(Int, String, mutable.ListBuffer[Entry])] = List((0, root_name, buffer()))
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    36
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    37
      @tailrec def close(level: Int => Boolean)
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    38
      {
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    39
        stack match {
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    40
          case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    41
            body2 += Block(name, body.toList)
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    42
            stack = stack.tail
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    43
            close(level)
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    44
          case _ =>
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    45
        }
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    46
      }
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    47
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    48
      def result(): Entry =
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    49
      {
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    50
        close(_ => true)
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    51
        val (_, name, body) = stack.head
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    52
        Block(name, body.toList)
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    53
      }
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    54
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    55
      def add(command: Command)
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    56
      {
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    57
        syntax.heading_level(command) match {
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    58
          case Some(i) =>
40457
3b0050718b31 proper treatment of equal heading level;
wenzelm
parents: 40454
diff changeset
    59
            close(_ >= i)
40454
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    60
            stack = (i, command.source, buffer()) :: stack
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    61
          case None =>
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    62
        }
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    63
        stack.head._3 += Atom(command)
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    64
      }
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    65
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    66
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    67
      /* result structure */
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    68
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    69
      val spans = parse_spans(syntax.scan(text))
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    70
      spans.foreach(span => add(Command.span(span)))
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    71
      result()
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    72
    }
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    73
  }
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    74
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    75
2516ea25a54b some support for nested source structure, based on section headings;
wenzelm
parents: 38878
diff changeset
    76
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
    77
  /** parse spans **/
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
    78
38373
wenzelm
parents: 38239
diff changeset
    79
  def parse_spans(toks: List[Token]): List[List[Token]] =
34268
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
    80
  {
38373
wenzelm
parents: 38239
diff changeset
    81
    val result = new mutable.ListBuffer[List[Token]]
38239
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    82
    val span = new mutable.ListBuffer[Token]
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    83
    val whitespace = new mutable.ListBuffer[Token]
34268
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
    84
38239
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    85
    def flush(buffer: mutable.ListBuffer[Token])
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    86
    {
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    87
      if (!buffer.isEmpty) { result += buffer.toList; buffer.clear }
34268
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
    88
    }
38239
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    89
    for (tok <- toks) {
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    90
      if (tok.is_command) { flush(span); flush(whitespace); span += tok }
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    91
      else if (tok.is_ignored) whitespace += tok
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    92
      else { span ++= whitespace; whitespace.clear; span += tok }
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    93
    }
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    94
    flush(span); flush(whitespace)
89a4d1028fb3 parse_spans: somewhat faster low-level implementation;
wenzelm
parents: 36956
diff changeset
    95
    result.toList
34268
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
    96
  }
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
    97
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
    98
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
    99
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   100
  /** perspective **/
44388
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   101
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   102
  def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   103
  {
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44473
diff changeset
   104
    if (perspective.is_empty) Command.Perspective.empty
44388
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   105
    else {
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   106
      val result = new mutable.ListBuffer[Command]
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   107
      @tailrec
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   108
      def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   109
      {
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   110
        (ranges, commands) match {
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   111
          case (range :: more_ranges, (command, offset) #:: more_commands) =>
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   112
            val command_range = command.range + offset
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   113
            range compare command_range match {
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   114
              case -1 => check_ranges(more_ranges, commands)
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   115
              case 0 =>
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   116
                result += command
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   117
                check_ranges(ranges, more_commands)
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   118
              case 1 => check_ranges(ranges, more_commands)
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   119
            }
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   120
          case _ =>
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   121
        }
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   122
      }
44473
4f264fdf8d0e slightly more abstract Text.Perspective;
wenzelm
parents: 44443
diff changeset
   123
      check_ranges(perspective.ranges, node.command_range(perspective.range).toStream)
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44473
diff changeset
   124
      Command.Perspective(result.toList)
44388
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   125
    }
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   126
  }
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   127
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   128
  def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   129
    : (Command.Perspective, Option[Document.Nodes]) =
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   130
  {
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   131
    val node = nodes(name)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   132
    val perspective = command_perspective(node, text_perspective)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   133
    val new_nodes =
44474
681447a9ffe5 slightly more abstract Command.Perspective;
wenzelm
parents: 44473
diff changeset
   134
      if (node.perspective same perspective) None
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   135
      else Some(nodes + (name -> node.copy(perspective = perspective)))
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   136
    (perspective, new_nodes)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   137
  }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   138
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   139
  def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   140
    : (Command.Perspective, Document.Version) =
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   141
  {
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   142
    val nodes = previous.nodes
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   143
    val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   144
    val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   145
    (perspective, version)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   146
  }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   147
44388
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   148
5f9ad3583e0a tuned signature;
wenzelm
parents: 44385
diff changeset
   149
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   150
  /** text edits **/
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   151
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43715
diff changeset
   152
  def text_edits(
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43715
diff changeset
   153
      syntax: Outer_Syntax,
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43715
diff changeset
   154
      previous: Document.Version,
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   155
      edits: List[Document.Edit_Text])
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   156
    : (List[Document.Edit_Command], Document.Version) =
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   157
  {
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   158
    /* phase 1: edit individual command source */
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   159
38425
e467db701d78 moved Text_Edit to Text.Edit;
wenzelm
parents: 38419
diff changeset
   160
    @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   161
        : Linear_Set[Command] =
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   162
    {
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   163
      eds match {
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   164
        case e :: es =>
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   165
          Document.Node.command_starts(commands.iterator).find {
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   166
            case (cmd, cmd_start) =>
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   167
              e.can_edit(cmd.source, cmd_start) ||
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   168
                e.is_insert && e.start == cmd_start + cmd.length
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   169
          } match {
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   170
            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   171
              val (rest, text) = e.edit(cmd.source, cmd_start)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   172
              val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   173
              edit_text(rest.toList ::: es, new_commands)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   174
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   175
            case Some((cmd, cmd_start)) =>
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   176
              edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   177
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   178
            case None =>
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   179
              require(e.is_insert && e.start == 0)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   180
              edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   181
          }
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   182
        case Nil => commands
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   183
      }
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   184
    }
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   185
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   186
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   187
    /* phase 2: recover command spans */
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   188
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   189
    @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   190
    {
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44185
diff changeset
   191
      commands.iterator.find(cmd => !cmd.is_defined) match {
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   192
        case Some(first_unparsed) =>
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   193
          val first =
38878
1d5b3175fd30 text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;
wenzelm
parents: 38569
diff changeset
   194
            commands.reverse_iterator(first_unparsed).
1d5b3175fd30 text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;
wenzelm
parents: 38569
diff changeset
   195
              dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   196
          val last =
38878
1d5b3175fd30 text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;
wenzelm
parents: 38569
diff changeset
   197
            commands.iterator(first_unparsed).
1d5b3175fd30 text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;
wenzelm
parents: 38569
diff changeset
   198
              dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   199
          val range =
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   200
            commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   201
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   202
          val sources = range.flatMap(_.span.map(_.source))
43647
42b98a59ec30 tuned signature;
wenzelm
parents: 40792
diff changeset
   203
          val spans0 = parse_spans(syntax.scan(sources.mkString))
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   204
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   205
          val (before_edit, spans1) =
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   206
            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   207
              (Some(first), spans0.tail)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   208
            else (commands.prev(first), spans0)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   209
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   210
          val (after_edit, spans2) =
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   211
            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   212
              (Some(last), spans1.take(spans1.length - 1))
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   213
            else (commands.next(last), spans1)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   214
43662
e3175ec00311 Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
wenzelm
parents: 43660
diff changeset
   215
          val inserted = spans2.map(span => new Command(Document.new_id(), span))
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   216
          val new_commands =
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   217
            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   218
          recover_spans(new_commands)
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   219
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   220
        case None => commands
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   221
      }
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   222
    }
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   223
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   224
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   225
    /* resulting document edits */
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   226
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   227
    {
40479
cc06f5528bb1 unified type Document.Edit;
wenzelm
parents: 40478
diff changeset
   228
      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
38417
b8922ae21111 renamed class Document to Document.Version etc.;
wenzelm
parents: 38374
diff changeset
   229
      var nodes = previous.nodes
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   230
40478
4bae781b8f7c replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents: 40457
diff changeset
   231
      edits foreach {
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44182
diff changeset
   232
        case (name, Document.Node.Clear()) =>
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44182
diff changeset
   233
          doc_edits += (name -> Document.Node.Clear())
44443
35d67b2056cc clarified Document.Node.clear -- retain header (cf. ML version);
wenzelm
parents: 44436
diff changeset
   234
          nodes += (name -> nodes(name).clear)
40478
4bae781b8f7c replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents: 40457
diff changeset
   235
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43722
diff changeset
   236
        case (name, Document.Node.Edits(text_edits)) =>
43697
77ce24aa1770 explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents: 43662
diff changeset
   237
          val node = nodes(name)
77ce24aa1770 explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents: 43662
diff changeset
   238
          val commands0 = node.commands
40478
4bae781b8f7c replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents: 40457
diff changeset
   239
          val commands1 = edit_text(text_edits, commands0)
4bae781b8f7c replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents: 40457
diff changeset
   240
          val commands2 = recover_spans(commands1)   // FIXME somewhat slow
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   241
40478
4bae781b8f7c replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents: 40457
diff changeset
   242
          val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
4bae781b8f7c replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents: 40457
diff changeset
   243
          val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   244
40478
4bae781b8f7c replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents: 40457
diff changeset
   245
          val cmd_edits =
4bae781b8f7c replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents: 40457
diff changeset
   246
            removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
4bae781b8f7c replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents: 40457
diff changeset
   247
            inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   248
44156
6aa25b80e1a5 explicit datatypes for document node edits;
wenzelm
parents: 43722
diff changeset
   249
          doc_edits += (name -> Document.Node.Edits(cmd_edits))
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   250
          nodes += (name -> node.copy(commands = commands2))
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43715
diff changeset
   251
44182
ecb51b457064 clarified node header -- exclude master_dir;
wenzelm
parents: 44180
diff changeset
   252
        case (name, Document.Node.Header(header)) =>
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   253
          val node = nodes(name)
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   254
          val update_header =
44182
ecb51b457064 clarified node header -- exclude master_dir;
wenzelm
parents: 44180
diff changeset
   255
            (node.header, header) match {
ecb51b457064 clarified node header -- exclude master_dir;
wenzelm
parents: 44180
diff changeset
   256
              case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header
44160
8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents: 44157
diff changeset
   257
              case _ => true
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   258
            }
44180
a6dc270d3edb maintain node header;
wenzelm
parents: 44160
diff changeset
   259
          if (update_header) {
44182
ecb51b457064 clarified node header -- exclude master_dir;
wenzelm
parents: 44180
diff changeset
   260
            doc_edits += (name -> Document.Node.Header(header))
44180
a6dc270d3edb maintain node header;
wenzelm
parents: 44160
diff changeset
   261
            nodes += (name -> node.copy(header = header))
a6dc270d3edb maintain node header;
wenzelm
parents: 44160
diff changeset
   262
          }
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44185
diff changeset
   263
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44185
diff changeset
   264
        case (name, Document.Node.Perspective(text_perspective)) =>
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   265
          update_perspective(nodes, name, text_perspective) match {
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   266
            case (_, None) =>
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   267
            case (perspective, Some(nodes1)) =>
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   268
              doc_edits += (name -> Document.Node.Perspective(perspective))
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44388
diff changeset
   269
              nodes = nodes1
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44185
diff changeset
   270
          }
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   271
      }
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   272
      (doc_edits.toList, Document.Version(Document.new_id(), nodes))
38374
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   273
    }
7eb0f6991e25 moved Document.text_edits to Thy_Syntax;
wenzelm
parents: 38373
diff changeset
   274
  }
34268
b149b7083236 separate module Thy_Syntax for command span parsing;
wenzelm
parents:
diff changeset
   275
}