maintain document model for all files, with document view for theory only, and special blob for non-theory files;
authorwenzelm
Mon Nov 18 17:16:56 2013 +0100 (2013-11-18)
changeset 545091f77110c94ef
parent 54467 663a927fdc88
child 54510 865712316b5f
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_thy_load.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Nov 18 09:45:50 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Nov 18 17:16:56 2013 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4    visible_last = try List.last command_ids,
     1.5    overlays = Inttab.make_list overlays};
     1.6  
     1.7 -val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
     1.8 +val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["No theory header"]);
     1.9  val no_perspective = make_perspective (false, [], []);
    1.10  
    1.11  val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
     2.1 --- a/src/Pure/PIDE/document.scala	Mon Nov 18 09:45:50 2013 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Mon Nov 18 17:16:56 2013 +0100
     2.3 @@ -64,6 +64,8 @@
     2.4  
     2.5      def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
     2.6  
     2.7 +    val no_header = bad_header("No theory header")
     2.8 +
     2.9      object Name
    2.10      {
    2.11        val empty = Name("", "", "")
    2.12 @@ -83,6 +85,8 @@
    2.13            case _ => false
    2.14          }
    2.15        override def toString: String = theory
    2.16 +
    2.17 +      def is_theory: Boolean = !theory.isEmpty
    2.18      }
    2.19  
    2.20  
    2.21 @@ -121,6 +125,7 @@
    2.22      case class Edits[A, B](edits: List[A]) extends Edit[A, B]
    2.23      case class Deps[A, B](header: Header) extends Edit[A, B]
    2.24      case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
    2.25 +    case class Blob[A, B](blob: Bytes) extends Edit[A, B]
    2.26      type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
    2.27      type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
    2.28  
    2.29 @@ -184,27 +189,31 @@
    2.30      val header: Node.Header = Node.bad_header("Bad theory header"),
    2.31      val perspective: Node.Perspective_Command =
    2.32        Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
    2.33 +    val blob: Bytes = Bytes.empty,
    2.34      _commands: Node.Commands = Node.Commands.empty)
    2.35    {
    2.36      def clear: Node = new Node(header = header)
    2.37  
    2.38      def update_header(new_header: Node.Header): Node =
    2.39 -      new Node(new_header, perspective, _commands)
    2.40 +      new Node(new_header, perspective, blob, _commands)
    2.41  
    2.42      def update_perspective(new_perspective: Node.Perspective_Command): Node =
    2.43 -      new Node(header, new_perspective, _commands)
    2.44 +      new Node(header, new_perspective, blob, _commands)
    2.45  
    2.46      def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
    2.47        perspective.required == other_perspective.required &&
    2.48        perspective.visible.same(other_perspective.visible) &&
    2.49        perspective.overlays == other_perspective.overlays
    2.50  
    2.51 +    def update_blob(new_blob: Bytes): Node =
    2.52 +      new Node(header, perspective, new_blob, _commands)
    2.53 +
    2.54      def commands: Linear_Set[Command] = _commands.commands
    2.55      def thy_load_commands: List[Command] = _commands.thy_load_commands
    2.56  
    2.57      def update_commands(new_commands: Linear_Set[Command]): Node =
    2.58        if (new_commands eq _commands.commands) this
    2.59 -      else new Node(header, perspective, Node.Commands(new_commands))
    2.60 +      else new Node(header, perspective, blob, Node.Commands(new_commands))
    2.61  
    2.62      def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    2.63        _commands.range(i)
     3.1 --- a/src/Pure/PIDE/protocol.scala	Mon Nov 18 09:45:50 2013 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Nov 18 17:16:56 2013 +0100
     3.3 @@ -335,6 +335,7 @@
     3.4        def encode_edit(name: Document.Node.Name)
     3.5            : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
     3.6          variant(List(
     3.7 +          // FIXME Document.Node.Blob (!??)
     3.8            { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
     3.9            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
    3.10            { case Document.Node.Deps(header) =>
     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 09:45:50 2013 +0100
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 17:16:56 2013 +0100
     4.3 @@ -355,6 +355,8 @@
     4.4          else
     4.5            node.update_perspective(perspective).update_commands(
     4.6              consolidate_spans(syntax, reparse_limit, name, visible, node.commands))
     4.7 +
     4.8 +      case (_, Document.Node.Blob(blob)) => node.update_blob(blob)
     4.9      }
    4.10    }
    4.11  
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Nov 18 09:45:50 2013 +0100
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Nov 18 17:16:56 2013 +0100
     5.3 @@ -60,17 +60,23 @@
     5.4  {
     5.5    /* header */
     5.6  
     5.7 +  def is_theory: Boolean = node_name.is_theory
     5.8 +
     5.9    def node_header(): Document.Node.Header =
    5.10    {
    5.11      Swing_Thread.require()
    5.12 -    JEdit_Lib.buffer_lock(buffer) {
    5.13 -      Exn.capture {
    5.14 -        PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
    5.15 -      } match {
    5.16 -        case Exn.Res(header) => header
    5.17 -        case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
    5.18 +
    5.19 +    if (is_theory) {
    5.20 +      JEdit_Lib.buffer_lock(buffer) {
    5.21 +        Exn.capture {
    5.22 +          PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
    5.23 +        } match {
    5.24 +          case Exn.Res(header) => header
    5.25 +          case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
    5.26 +        }
    5.27        }
    5.28      }
    5.29 +    else Document.Node.no_header
    5.30    }
    5.31  
    5.32  
    5.33 @@ -96,7 +102,7 @@
    5.34    {
    5.35      Swing_Thread.require()
    5.36  
    5.37 -    if (Isabelle.continuous_checking) {
    5.38 +    if (Isabelle.continuous_checking && is_theory) {
    5.39        val snapshot = this.snapshot()
    5.40        Document.Node.Perspective(node_required, Text.Perspective(
    5.41          for {
    5.42 @@ -108,6 +114,14 @@
    5.43    }
    5.44  
    5.45  
    5.46 +  /* blob */
    5.47 +
    5.48 +  // FIXME caching
    5.49 +  // FIXME precise file content (encoding)
    5.50 +  def blob(): Bytes =
    5.51 +    Swing_Thread.require { Bytes(buffer.getText(0, buffer.getLength)) }
    5.52 +
    5.53 +
    5.54    /* edits */
    5.55  
    5.56    def init_edits(): List[Document.Edit_Text] =
    5.57 @@ -118,10 +132,13 @@
    5.58      val text = JEdit_Lib.buffer_text(buffer)
    5.59      val perspective = node_perspective()
    5.60  
    5.61 -    List(session.header_edit(node_name, header),
    5.62 -      node_name -> Document.Node.Clear(),
    5.63 -      node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
    5.64 -      node_name -> perspective)
    5.65 +    if (is_theory)
    5.66 +      List(session.header_edit(node_name, header),
    5.67 +        node_name -> Document.Node.Clear(),
    5.68 +        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
    5.69 +        node_name -> perspective)
    5.70 +    else
    5.71 +      List(node_name -> Document.Node.Blob(blob()))
    5.72    }
    5.73  
    5.74    def node_edits(
    5.75 @@ -131,16 +148,20 @@
    5.76    {
    5.77      Swing_Thread.require()
    5.78  
    5.79 -    val header_edit = session.header_edit(node_name, node_header())
    5.80 -    if (clear)
    5.81 -      List(header_edit,
    5.82 -        node_name -> Document.Node.Clear(),
    5.83 -        node_name -> Document.Node.Edits(text_edits),
    5.84 -        node_name -> perspective)
    5.85 +    if (is_theory) {
    5.86 +      val header_edit = session.header_edit(node_name, node_header())
    5.87 +      if (clear)
    5.88 +        List(header_edit,
    5.89 +          node_name -> Document.Node.Clear(),
    5.90 +          node_name -> Document.Node.Edits(text_edits),
    5.91 +          node_name -> perspective)
    5.92 +      else
    5.93 +        List(header_edit,
    5.94 +          node_name -> Document.Node.Edits(text_edits),
    5.95 +          node_name -> perspective)
    5.96 +    }
    5.97      else
    5.98 -      List(header_edit,
    5.99 -        node_name -> Document.Node.Edits(text_edits),
   5.100 -        node_name -> perspective)
   5.101 +      List(node_name -> Document.Node.Blob(blob()))
   5.102    }
   5.103  
   5.104  
     6.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Nov 18 09:45:50 2013 +0100
     6.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Nov 18 17:16:56 2013 +0100
     6.3 @@ -133,15 +133,15 @@
     6.4  
     6.5  
     6.6  class Isabelle_Sidekick_Default extends
     6.7 -  Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.buffer_node_name)
     6.8 +  Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.theory_node_name)
     6.9  
    6.10  
    6.11  class Isabelle_Sidekick_Options extends
    6.12 -  Isabelle_Sidekick_Structure("isabelle-options", PIDE.thy_load.buffer_node_dummy)
    6.13 +  Isabelle_Sidekick_Structure("isabelle-options", b => Some(PIDE.thy_load.dummy_node_name(b)))
    6.14  
    6.15  
    6.16  class Isabelle_Sidekick_Root extends
    6.17 -  Isabelle_Sidekick_Structure("isabelle-root", PIDE.thy_load.buffer_node_dummy)
    6.18 +  Isabelle_Sidekick_Structure("isabelle-root", b => Some(PIDE.thy_load.dummy_node_name(b)))
    6.19  
    6.20  
    6.21  class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
     7.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Mon Nov 18 09:45:50 2013 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Mon Nov 18 17:16:56 2013 +0100
     7.3 @@ -22,13 +22,19 @@
     7.4  {
     7.5    /* document node names */
     7.6  
     7.7 -  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
     7.8 -    Some(Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName))
     7.9 +  def dummy_node_name(buffer: Buffer): Document.Node.Name =
    7.10 +    Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName)
    7.11  
    7.12 -  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
    7.13 +  def node_name(buffer: Buffer): Document.Node.Name =
    7.14    {
    7.15      val name = JEdit_Lib.buffer_name(buffer)
    7.16 -    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
    7.17 +    Document.Node.Name(name, buffer.getDirectory, Thy_Header.thy_name(name).getOrElse(""))
    7.18 +  }
    7.19 +
    7.20 +  def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
    7.21 +  {
    7.22 +    val name = node_name(buffer)
    7.23 +    if (name.is_theory) Some(name) else None
    7.24    }
    7.25  
    7.26  
     8.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Nov 18 09:45:50 2013 +0100
     8.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Nov 18 17:16:56 2013 +0100
     8.3 @@ -96,21 +96,18 @@
     8.4        val init_edits =
     8.5          (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
     8.6            JEdit_Lib.buffer_lock(buffer) {
     8.7 -            val (model_edits, opt_model) =
     8.8 -              thy_load.buffer_node_name(buffer) match {
     8.9 -                case Some(node_name) =>
    8.10 -                  document_model(buffer) match {
    8.11 -                    case Some(model) if model.node_name == node_name => (Nil, Some(model))
    8.12 -                    case _ =>
    8.13 -                      val model = Document_Model.init(session, buffer, node_name)
    8.14 -                      (model.init_edits(), Some(model))
    8.15 -                  }
    8.16 -                case None => (Nil, None)
    8.17 +            val node_name = thy_load.node_name(buffer)
    8.18 +            val (model_edits, model) =
    8.19 +              document_model(buffer) match {
    8.20 +                case Some(model) if model.node_name == node_name => (Nil, model)
    8.21 +                case _ =>
    8.22 +                  val model = Document_Model.init(session, buffer, node_name)
    8.23 +                  (model.init_edits(), model)
    8.24                }
    8.25 -            if (opt_model.isDefined) {
    8.26 +            if (model.is_theory) {
    8.27                for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
    8.28 -                if (document_view(text_area).map(_.model) != opt_model)
    8.29 -                  Document_View.init(opt_model.get, text_area)
    8.30 +                if (document_view(text_area).map(_.model) != Some(model))
    8.31 +                  Document_View.init(model, text_area)
    8.32                }
    8.33              }
    8.34              model_edits ::: edits
    8.35 @@ -124,8 +121,8 @@
    8.36    {
    8.37      JEdit_Lib.swing_buffer_lock(buffer) {
    8.38        document_model(buffer) match {
    8.39 -        case Some(model) => Document_View.init(model, text_area)
    8.40 -        case None =>
    8.41 +        case Some(model) if model.is_theory => Document_View.init(model, text_area)
    8.42 +        case _ =>
    8.43        }
    8.44      }
    8.45    }
    8.46 @@ -163,8 +160,11 @@
    8.47              buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
    8.48  
    8.49            val thys =
    8.50 -            for (buffer <- buffers; model <- PIDE.document_model(buffer))
    8.51 -              yield model.node_name
    8.52 +            for {
    8.53 +              buffer <- buffers
    8.54 +              model <- PIDE.document_model(buffer)
    8.55 +              if model.is_theory
    8.56 +            } yield model.node_name
    8.57  
    8.58            val thy_info = new Thy_Info(PIDE.thy_load)
    8.59            // FIXME avoid I/O in Swing thread!?!