src/Pure/Thy/thy_syntax.scala
author wenzelm
Tue Aug 12 00:17:02 2014 +0200 (2014-08-12)
changeset 57906 020df63dd0a9
parent 57905 c0c5652e796e
child 59077 7e0d3da6e6d8
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/Thy/thy_syntax.scala
     2     Author:     Makarius
     3 
     4 Superficial theory syntax: tokens and spans.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.mutable
    11 import scala.annotation.tailrec
    12 
    13 
    14 object Thy_Syntax
    15 {
    16   /** perspective **/
    17 
    18   def command_perspective(
    19       node: Document.Node,
    20       perspective: Text.Perspective,
    21       overlays: Document.Node.Overlays): (Command.Perspective, Command.Perspective) =
    22   {
    23     if (perspective.is_empty && overlays.is_empty)
    24       (Command.Perspective.empty, Command.Perspective.empty)
    25     else {
    26       val has_overlay = overlays.commands
    27       val visible = new mutable.ListBuffer[Command]
    28       val visible_overlay = new mutable.ListBuffer[Command]
    29       @tailrec
    30       def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
    31       {
    32         (ranges, commands) match {
    33           case (range :: more_ranges, (command, offset) #:: more_commands) =>
    34             val command_range = command.range + offset
    35             range compare command_range match {
    36               case 0 =>
    37                 visible += command
    38                 visible_overlay += command
    39                 check_ranges(ranges, more_commands)
    40               case c =>
    41                 if (has_overlay(command)) visible_overlay += command
    42 
    43                 if (c < 0) check_ranges(more_ranges, commands)
    44                 else check_ranges(ranges, more_commands)
    45             }
    46 
    47           case (Nil, (command, _) #:: more_commands) =>
    48             if (has_overlay(command)) visible_overlay += command
    49 
    50             check_ranges(Nil, more_commands)
    51 
    52           case _ =>
    53         }
    54       }
    55 
    56       val commands =
    57         (if (overlays.is_empty) node.command_iterator(perspective.range)
    58          else node.command_iterator()).toStream
    59       check_ranges(perspective.ranges, commands)
    60       (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
    61     }
    62   }
    63 
    64 
    65 
    66   /** header edits: structure and outer syntax **/
    67 
    68   private def header_edits(
    69     resources: Resources,
    70     previous: Document.Version,
    71     edits: List[Document.Edit_Text]):
    72     (Prover.Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
    73       List[Document.Edit_Command]) =
    74   {
    75     var updated_imports = false
    76     var updated_keywords = false
    77     var nodes = previous.nodes
    78     val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
    79 
    80     edits foreach {
    81       case (name, Document.Node.Deps(header)) =>
    82         val node = nodes(name)
    83         val update_header =
    84           !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header
    85         if (update_header) {
    86           val node1 = node.update_header(header)
    87           updated_imports = updated_imports || (node.header.imports != node1.header.imports)
    88           updated_keywords = updated_keywords || (node.header.keywords != node1.header.keywords)
    89           nodes += (name -> node1)
    90           doc_edits += (name -> Document.Node.Deps(header))
    91         }
    92       case _ =>
    93     }
    94 
    95     val (syntax, syntax_changed) =
    96       previous.syntax match {
    97         case Some(syntax) if !updated_keywords =>
    98           (syntax, false)
    99         case _ =>
   100           val syntax =
   101             (resources.base_syntax /: nodes.iterator) {
   102               case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
   103             }
   104           (syntax, true)
   105       }
   106 
   107     val reparse =
   108       if (updated_imports || updated_keywords)
   109         nodes.descendants(doc_edits.iterator.map(_._1).toList)
   110       else Nil
   111 
   112     (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList)
   113   }
   114 
   115 
   116 
   117   /** text edits **/
   118 
   119   /* edit individual command source */
   120 
   121   @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
   122   {
   123     eds match {
   124       case e :: es =>
   125         Document.Node.Commands.starts(commands.iterator).find {
   126           case (cmd, cmd_start) =>
   127             e.can_edit(cmd.source, cmd_start) ||
   128               e.is_insert && e.start == cmd_start + cmd.length
   129         } match {
   130           case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
   131             val (rest, text) = e.edit(cmd.source, cmd_start)
   132             val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
   133             edit_text(rest.toList ::: es, new_commands)
   134 
   135           case Some((cmd, cmd_start)) =>
   136             edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
   137 
   138           case None =>
   139             require(e.is_insert && e.start == 0)
   140             edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
   141         }
   142       case Nil => commands
   143     }
   144   }
   145 
   146 
   147   /* reparse range of command spans */
   148 
   149   @tailrec private def chop_common(
   150       cmds: List[Command],
   151       blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
   152     : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
   153   {
   154     (cmds, blobs_spans) match {
   155       case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
   156         chop_common(cmds, rest)
   157       case _ => (cmds, blobs_spans)
   158     }
   159   }
   160 
   161   private def reparse_spans(
   162     resources: Resources,
   163     syntax: Prover.Syntax,
   164     get_blob: Document.Node.Name => Option[Document.Blob],
   165     name: Document.Node.Name,
   166     commands: Linear_Set[Command],
   167     first: Command, last: Command): Linear_Set[Command] =
   168   {
   169     val cmds0 = commands.iterator(first, last).toList
   170     val blobs_spans0 =
   171       syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
   172         map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
   173 
   174     val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
   175 
   176     val (rev_cmds2, rev_blobs_spans2) = chop_common(cmds1.reverse, blobs_spans1.reverse)
   177     val cmds2 = rev_cmds2.reverse
   178     val blobs_spans2 = rev_blobs_spans2.reverse
   179 
   180     cmds2 match {
   181       case Nil =>
   182         assert(blobs_spans2.isEmpty)
   183         commands
   184       case cmd :: _ =>
   185         val hook = commands.prev(cmd)
   186         val inserted =
   187           blobs_spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
   188         (commands /: cmds2)(_ - _).append_after(hook, inserted)
   189     }
   190   }
   191 
   192 
   193   /* recover command spans after edits */
   194 
   195   // FIXME somewhat slow
   196   private def recover_spans(
   197     resources: Resources,
   198     syntax: Prover.Syntax,
   199     get_blob: Document.Node.Name => Option[Document.Blob],
   200     name: Document.Node.Name,
   201     perspective: Command.Perspective,
   202     commands: Linear_Set[Command]): Linear_Set[Command] =
   203   {
   204     val visible = perspective.commands.toSet
   205 
   206     def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
   207       cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || visible(cmd))
   208         .find(_.is_proper) getOrElse cmds.last
   209 
   210     @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
   211       cmds.find(_.is_unparsed) match {
   212         case Some(first_unparsed) =>
   213           val first = next_invisible_command(cmds.reverse, first_unparsed)
   214           val last = next_invisible_command(cmds, first_unparsed)
   215           recover(reparse_spans(resources, syntax, get_blob, name, cmds, first, last))
   216         case None => cmds
   217       }
   218     recover(commands)
   219   }
   220 
   221 
   222   /* consolidate unfinished spans */
   223 
   224   private def consolidate_spans(
   225     resources: Resources,
   226     syntax: Prover.Syntax,
   227     get_blob: Document.Node.Name => Option[Document.Blob],
   228     reparse_limit: Int,
   229     name: Document.Node.Name,
   230     perspective: Command.Perspective,
   231     commands: Linear_Set[Command]): Linear_Set[Command] =
   232   {
   233     if (perspective.commands.isEmpty) commands
   234     else {
   235       commands.find(_.is_unfinished) match {
   236         case Some(first_unfinished) =>
   237           val visible = perspective.commands.toSet
   238           commands.reverse.find(visible) match {
   239             case Some(last_visible) =>
   240               val it = commands.iterator(last_visible)
   241               var last = last_visible
   242               var i = 0
   243               while (i < reparse_limit && it.hasNext) {
   244                 last = it.next
   245                 i += last.length
   246               }
   247               reparse_spans(resources, syntax, get_blob, name, commands, first_unfinished, last)
   248             case None => commands
   249           }
   250         case None => commands
   251       }
   252     }
   253   }
   254 
   255 
   256   /* main */
   257 
   258   def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
   259     : List[Command.Edit] =
   260   {
   261     val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
   262     val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
   263 
   264     removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) :::
   265     inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
   266   }
   267 
   268   private def text_edit(
   269     resources: Resources,
   270     syntax: Prover.Syntax,
   271     get_blob: Document.Node.Name => Option[Document.Blob],
   272     reparse_limit: Int,
   273     node: Document.Node, edit: Document.Edit_Text): Document.Node =
   274   {
   275     edit match {
   276       case (_, Document.Node.Clear()) => node.clear
   277 
   278       case (_, Document.Node.Blob(blob)) => node.init_blob(blob)
   279 
   280       case (name, Document.Node.Edits(text_edits)) =>
   281         if (name.is_theory) {
   282           val commands0 = node.commands
   283           val commands1 = edit_text(text_edits, commands0)
   284           val commands2 =
   285             recover_spans(resources, syntax, get_blob, name, node.perspective.visible, commands1)
   286           node.update_commands(commands2)
   287         }
   288         else node
   289 
   290       case (_, Document.Node.Deps(_)) => node
   291 
   292       case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
   293         val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
   294         val perspective: Document.Node.Perspective_Command =
   295           Document.Node.Perspective(required, visible_overlay, overlays)
   296         if (node.same_perspective(perspective)) node
   297         else
   298           node.update_perspective(perspective).update_commands(
   299             consolidate_spans(resources, syntax, get_blob, reparse_limit,
   300               name, visible, node.commands))
   301     }
   302   }
   303 
   304   def parse_change(
   305       resources: Resources,
   306       reparse_limit: Int,
   307       previous: Document.Version,
   308       doc_blobs: Document.Blobs,
   309       edits: List[Document.Edit_Text]): Session.Change =
   310   {
   311     def get_blob(name: Document.Node.Name) =
   312       doc_blobs.get(name) orElse previous.nodes(name).get_blob
   313 
   314     val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
   315       header_edits(resources, previous, edits)
   316 
   317     val (doc_edits, version) =
   318       if (edits.isEmpty) (Nil, Document.Version.make(Some(syntax), previous.nodes))
   319       else {
   320         val reparse =
   321           (reparse0 /: nodes0.iterator)({
   322             case (reparse, (name, node)) =>
   323               if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
   324                 name :: reparse
   325               else reparse
   326             })
   327         val reparse_set = reparse.toSet
   328 
   329         var nodes = nodes0
   330         val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
   331 
   332         val node_edits =
   333           (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
   334             .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
   335 
   336         node_edits foreach {
   337           case (name, edits) =>
   338             val node = nodes(name)
   339             val commands = node.commands
   340 
   341             val node1 =
   342               if (reparse_set(name) && !commands.isEmpty)
   343                 node.update_commands(
   344                   reparse_spans(resources, syntax, get_blob,
   345                     name, commands, commands.head, commands.last))
   346               else node
   347             val node2 =
   348               (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _))
   349 
   350             if (!(node.same_perspective(node2.perspective)))
   351               doc_edits += (name -> node2.perspective)
   352 
   353             doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
   354 
   355             nodes += (name -> node2)
   356         }
   357         (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes))
   358       }
   359 
   360     Session.Change(previous, syntax_changed, deps_changed, doc_edits, version)
   361   }
   362 }