src/Pure/Thy/thy_syntax.scala
author wenzelm
Tue Nov 19 13:54:02 2013 +0100 (2013-11-19)
changeset 54518 81a9a54c57fc
parent 54517 044bee8c5e69
child 54519 5fed81762406
permissions -rw-r--r--
always reparse nodes with thy_load commands, to update inlined files;
     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   /** nested structure **/
    17 
    18   object Structure
    19   {
    20     sealed abstract class Entry { def length: Int }
    21     case class Block(val name: String, val body: List[Entry]) extends Entry
    22     {
    23       val length: Int = (0 /: body)(_ + _.length)
    24     }
    25     case class Atom(val command: Command) extends Entry
    26     {
    27       def length: Int = command.length
    28     }
    29 
    30     def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
    31     {
    32       /* stack operations */
    33 
    34       def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
    35       var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
    36         List((0, node_name.toString, buffer()))
    37 
    38       @tailrec def close(level: Int => Boolean)
    39       {
    40         stack match {
    41           case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
    42             body2 += Block(name, body.toList)
    43             stack = stack.tail
    44             close(level)
    45           case _ =>
    46         }
    47       }
    48 
    49       def result(): Entry =
    50       {
    51         close(_ => true)
    52         val (_, name, body) = stack.head
    53         Block(name, body.toList)
    54       }
    55 
    56       def add(command: Command)
    57       {
    58         syntax.heading_level(command) match {
    59           case Some(i) =>
    60             close(_ > i)
    61             stack = (i + 1, command.source, buffer()) :: stack
    62           case None =>
    63         }
    64         stack.head._3 += Atom(command)
    65       }
    66 
    67 
    68       /* result structure */
    69 
    70       val spans = parse_spans(syntax.scan(text))
    71       spans.foreach(span => add(Command(Document_ID.none, node_name, span, Nil)))
    72       result()
    73     }
    74   }
    75 
    76 
    77 
    78   /** parse spans **/
    79 
    80   def parse_spans(toks: List[Token]): List[List[Token]] =
    81   {
    82     val result = new mutable.ListBuffer[List[Token]]
    83     val span = new mutable.ListBuffer[Token]
    84     val improper = new mutable.ListBuffer[Token]
    85 
    86     def flush()
    87     {
    88       if (!span.isEmpty) { result += span.toList; span.clear }
    89       if (!improper.isEmpty) { result += improper.toList; improper.clear }
    90     }
    91     for (tok <- toks) {
    92       if (tok.is_command) { flush(); span += tok }
    93       else if (tok.is_improper) improper += tok
    94       else { span ++= improper; improper.clear; span += tok }
    95     }
    96     flush()
    97 
    98     result.toList
    99   }
   100 
   101 
   102 
   103   /** perspective **/
   104 
   105   def command_perspective(
   106       node: Document.Node,
   107       perspective: Text.Perspective,
   108       overlays: Document.Node.Overlays): (Command.Perspective, Command.Perspective) =
   109   {
   110     if (perspective.is_empty && overlays.is_empty)
   111       (Command.Perspective.empty, Command.Perspective.empty)
   112     else {
   113       val has_overlay = overlays.commands
   114       val visible = new mutable.ListBuffer[Command]
   115       val visible_overlay = new mutable.ListBuffer[Command]
   116       @tailrec
   117       def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
   118       {
   119         (ranges, commands) match {
   120           case (range :: more_ranges, (command, offset) #:: more_commands) =>
   121             val command_range = command.range + offset
   122             range compare command_range match {
   123               case 0 =>
   124                 visible += command
   125                 visible_overlay += command
   126                 check_ranges(ranges, more_commands)
   127               case c =>
   128                 if (has_overlay(command)) visible_overlay += command
   129 
   130                 if (c < 0) check_ranges(more_ranges, commands)
   131                 else check_ranges(ranges, more_commands)
   132             }
   133 
   134           case (Nil, (command, _) #:: more_commands) =>
   135             if (has_overlay(command)) visible_overlay += command
   136 
   137             check_ranges(Nil, more_commands)
   138 
   139           case _ =>
   140         }
   141       }
   142 
   143       val commands =
   144         if (overlays.is_empty) node.command_range(perspective.range)
   145         else node.command_range()
   146       check_ranges(perspective.ranges, commands.toStream)
   147       (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
   148     }
   149   }
   150 
   151 
   152 
   153   /** header edits: structure and outer syntax **/
   154 
   155   private def header_edits(
   156     base_syntax: Outer_Syntax,
   157     previous: Document.Version,
   158     edits: List[Document.Edit_Text])
   159     : (Outer_Syntax, List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
   160   {
   161     var updated_imports = false
   162     var updated_keywords = false
   163     var nodes = previous.nodes
   164     val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
   165 
   166     edits foreach {
   167       case (name, Document.Node.Deps(header)) =>
   168         val node = nodes(name)
   169         val update_header =
   170           !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header
   171         if (update_header) {
   172           val node1 = node.update_header(header)
   173           updated_imports = updated_imports || (node.header.imports != node1.header.imports)
   174           updated_keywords = updated_keywords || (node.header.keywords != node1.header.keywords)
   175           nodes += (name -> node1)
   176           doc_edits += (name -> Document.Node.Deps(header))
   177         }
   178       case _ =>
   179     }
   180 
   181     val syntax =
   182       if (previous.is_init || updated_keywords)
   183         (base_syntax /: nodes.entries) {
   184           case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
   185         }
   186       else previous.syntax
   187 
   188     val reparse =
   189       if (updated_imports || updated_keywords)
   190         nodes.descendants(doc_edits.iterator.map(_._1).toList)
   191       else Nil
   192 
   193     (syntax, reparse, nodes, doc_edits.toList)
   194   }
   195 
   196 
   197 
   198   /** text edits **/
   199 
   200   /* edit individual command source */
   201 
   202   @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
   203   {
   204     eds match {
   205       case e :: es =>
   206         Document.Node.Commands.starts(commands.iterator).find {
   207           case (cmd, cmd_start) =>
   208             e.can_edit(cmd.source, cmd_start) ||
   209               e.is_insert && e.start == cmd_start + cmd.length
   210         } match {
   211           case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
   212             val (rest, text) = e.edit(cmd.source, cmd_start)
   213             val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
   214             edit_text(rest.toList ::: es, new_commands)
   215 
   216           case Some((cmd, cmd_start)) =>
   217             edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
   218 
   219           case None =>
   220             require(e.is_insert && e.start == 0)
   221             edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
   222         }
   223       case Nil => commands
   224     }
   225   }
   226 
   227 
   228   /* inlined files */
   229 
   230   private def find_file(tokens: List[Token]): Option[String] =
   231   {
   232     def clean(toks: List[Token]): List[Token] =
   233       toks match {
   234         case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
   235         case t :: ts => t :: clean(ts)
   236         case Nil => Nil
   237       }
   238     val clean_tokens = clean(tokens.filter(_.is_proper))
   239     clean_tokens.reverse.find(_.is_name).map(_.content)
   240   }
   241 
   242   def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =
   243     syntax.thy_load(span) match {
   244       case Some(exts) =>
   245         find_file(span) match {
   246           case Some(file) =>
   247             if (exts.isEmpty) List(file)
   248             else exts.map(ext => file + "." + ext)
   249           case None => Nil
   250         }
   251       case None => Nil
   252     }
   253 
   254   def resolve_files(
   255       thy_load: Thy_Load,
   256       syntax: Outer_Syntax,
   257       node_name: Document.Node.Name,
   258       span: List[Token],
   259       all_blobs: Map[Document.Node.Name, Bytes])
   260     : Command.Blobs =
   261   {
   262     span_files(syntax, span).map(file =>
   263       Exn.capture {
   264         val name =
   265           Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
   266         all_blobs.get(name) match {
   267           case Some(blob) => (name, blob.sha1_digest)
   268           case None => error("Bad file: " + quote(name.toString))
   269         }
   270       }
   271     )
   272   }
   273 
   274 
   275   /* reparse range of command spans */
   276 
   277   @tailrec private def chop_common(
   278       cmds: List[Command], spans: List[(List[Token], Command.Blobs)])
   279       : (List[Command], List[(List[Token], Command.Blobs)]) =
   280     (cmds, spans) match {
   281       case (c :: cs, (span, blobs) :: ps) if c.span == span && c.blobs == blobs =>
   282         chop_common(cs, ps)
   283       case _ => (cmds, spans)
   284     }
   285 
   286   private def reparse_spans(
   287     thy_load: Thy_Load,
   288     syntax: Outer_Syntax,
   289     all_blobs: Map[Document.Node.Name, Bytes],
   290     name: Document.Node.Name,
   291     commands: Linear_Set[Command],
   292     first: Command, last: Command): Linear_Set[Command] =
   293   {
   294     val cmds0 = commands.iterator(first, last).toList
   295     val spans0 =
   296       parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
   297         map(span => (span, resolve_files(thy_load, syntax, name, span, all_blobs)))
   298 
   299     val (cmds1, spans1) = chop_common(cmds0, spans0)
   300 
   301     val (rev_cmds2, rev_spans2) = chop_common(cmds1.reverse, spans1.reverse)
   302     val cmds2 = rev_cmds2.reverse
   303     val spans2 = rev_spans2.reverse
   304 
   305     cmds2 match {
   306       case Nil =>
   307         assert(spans2.isEmpty)
   308         commands
   309       case cmd :: _ =>
   310         val hook = commands.prev(cmd)
   311         val inserted =
   312           spans2.map({ case (span, blobs) => Command(Document_ID.make(), name, span, blobs) })
   313         (commands /: cmds2)(_ - _).append_after(hook, inserted)
   314     }
   315   }
   316 
   317 
   318   /* recover command spans after edits */
   319 
   320   // FIXME somewhat slow
   321   private def recover_spans(
   322     thy_load: Thy_Load,
   323     syntax: Outer_Syntax,
   324     all_blobs: Map[Document.Node.Name, Bytes],
   325     name: Document.Node.Name,
   326     perspective: Command.Perspective,
   327     commands: Linear_Set[Command]): Linear_Set[Command] =
   328   {
   329     val visible = perspective.commands.toSet
   330 
   331     def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
   332       cmds.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
   333         .find(_.is_command) getOrElse cmds.last
   334 
   335     @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
   336       cmds.find(_.is_unparsed) match {
   337         case Some(first_unparsed) =>
   338           val first = next_invisible_command(cmds.reverse, first_unparsed)
   339           val last = next_invisible_command(cmds, first_unparsed)
   340           recover(reparse_spans(thy_load, syntax, all_blobs, name, cmds, first, last))
   341         case None => cmds
   342       }
   343     recover(commands)
   344   }
   345 
   346 
   347   /* consolidate unfinished spans */
   348 
   349   private def consolidate_spans(
   350     thy_load: Thy_Load,
   351     syntax: Outer_Syntax,
   352     all_blobs: Map[Document.Node.Name, Bytes],
   353     reparse_limit: Int,
   354     name: Document.Node.Name,
   355     perspective: Command.Perspective,
   356     commands: Linear_Set[Command]): Linear_Set[Command] =
   357   {
   358     if (perspective.commands.isEmpty) commands
   359     else {
   360       commands.find(_.is_unfinished) match {
   361         case Some(first_unfinished) =>
   362           val visible = perspective.commands.toSet
   363           commands.reverse.find(visible) match {
   364             case Some(last_visible) =>
   365               val it = commands.iterator(last_visible)
   366               var last = last_visible
   367               var i = 0
   368               while (i < reparse_limit && it.hasNext) {
   369                 last = it.next
   370                 i += last.length
   371               }
   372               reparse_spans(thy_load, syntax, all_blobs, name, commands, first_unfinished, last)
   373             case None => commands
   374           }
   375         case None => commands
   376       }
   377     }
   378   }
   379 
   380 
   381   /* main */
   382 
   383   def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
   384     : List[Command.Edit] =
   385   {
   386     val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
   387     val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
   388 
   389     removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) :::
   390     inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
   391   }
   392 
   393   private def text_edit(
   394     thy_load: Thy_Load,
   395     syntax: Outer_Syntax,
   396     all_blobs: Map[Document.Node.Name, Bytes],
   397     reparse_limit: Int,
   398     node: Document.Node, edit: Document.Edit_Text): Document.Node =
   399   {
   400     edit match {
   401       case (_, Document.Node.Clear()) => node.clear
   402 
   403       case (name, Document.Node.Edits(text_edits)) =>
   404         val commands0 = node.commands
   405         val commands1 = edit_text(text_edits, commands0)
   406         val commands2 =
   407           recover_spans(thy_load, syntax, all_blobs, name, node.perspective.visible, commands1)
   408         node.update_commands(commands2)
   409 
   410       case (_, Document.Node.Deps(_)) => node
   411 
   412       case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
   413         val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
   414         val perspective: Document.Node.Perspective_Command =
   415           Document.Node.Perspective(required, visible_overlay, overlays)
   416         if (node.same_perspective(perspective)) node
   417         else
   418           node.update_perspective(perspective).update_commands(
   419             consolidate_spans(thy_load, syntax, all_blobs, reparse_limit,
   420               name, visible, node.commands))
   421 
   422       case (_, Document.Node.Blob(_)) => node
   423     }
   424   }
   425 
   426   def text_edits(
   427       thy_load: Thy_Load,
   428       reparse_limit: Int,
   429       previous: Document.Version,
   430       edits: List[Document.Edit_Text])
   431     : (List[Document.Edit_Command], Document.Version) =
   432   {
   433     val (syntax, reparse0, nodes0, doc_edits0) =
   434       header_edits(thy_load.base_syntax, previous, edits)
   435 
   436     val reparse =
   437       (reparse0 /: nodes0.entries)({
   438         case (reparse, (name, node)) =>
   439           if (node.thy_load_commands.isEmpty) reparse
   440           else name :: reparse
   441         })
   442     val reparse_set = reparse.toSet
   443 
   444     var nodes = nodes0
   445     val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
   446 
   447     val node_edits =
   448       (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
   449         .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
   450 
   451     val all_blobs: Map[Document.Node.Name, Bytes] =
   452       (Map.empty[Document.Node.Name, Bytes] /: node_edits) {
   453         case (bs1, (_, es)) => (bs1 /: es) {
   454           case (bs, (name, Document.Node.Blob(blob))) => bs + (name -> blob)
   455           case (bs, _) => bs
   456         }
   457       }
   458 
   459     node_edits foreach {
   460       case (name, edits) =>
   461         val node = nodes(name)
   462         val commands = node.commands
   463 
   464         val node1 =
   465           if (reparse_set(name) && !commands.isEmpty)
   466             node.update_commands(
   467               reparse_spans(thy_load, syntax, all_blobs,
   468                 name, commands, commands.head, commands.last))
   469           else node
   470         val node2 = (node1 /: edits)(text_edit(thy_load, syntax, all_blobs, reparse_limit, _, _))
   471 
   472         if (!(node.same_perspective(node2.perspective)))
   473           doc_edits += (name -> node2.perspective)
   474 
   475         doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
   476 
   477         nodes += (name -> node2)
   478     }
   479 
   480     (doc_edits.toList, Document.Version.make(syntax, nodes))
   481   }
   482 }