clarified modules;
authorwenzelm
Tue Nov 29 20:18:02 2011 +0100 (2011-11-29)
changeset 45672a497c5d4a523
parent 45671 1c769a2a2421
child 45673 cd41e3903fbf
clarified modules;
src/Pure/IsaMakefile
src/Pure/PIDE/command.scala
src/Pure/PIDE/isabelle_document.ML
src/Pure/PIDE/isabelle_document.scala
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Pure/build-jars
src/Tools/jEdit/src/isabelle_hyperlinks.scala
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/IsaMakefile	Tue Nov 29 20:17:11 2011 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Tue Nov 29 20:18:02 2011 +0100
     1.3 @@ -154,8 +154,8 @@
     1.4    ML/ml_syntax.ML					\
     1.5    ML/ml_thms.ML						\
     1.6    PIDE/document.ML					\
     1.7 +  PIDE/isabelle_document.ML				\
     1.8    PIDE/isabelle_markup.ML				\
     1.9 -  PIDE/isar_document.ML					\
    1.10    PIDE/markup.ML					\
    1.11    PIDE/xml.ML						\
    1.12    PIDE/yxml.ML						\
     2.1 --- a/src/Pure/PIDE/command.scala	Tue Nov 29 20:17:11 2011 +0100
     2.2 +++ b/src/Pure/PIDE/command.scala	Tue Nov 29 20:18:02 2011 +0100
     2.3 @@ -66,11 +66,11 @@
     2.4                val result = XML.Elem(Markup(name, Position.purge(atts)), body)
     2.5                val st0 = add_result(i, result)
     2.6                val st1 =
     2.7 -                if (Isar_Document.is_tracing(message)) st0
     2.8 +                if (Isabelle_Document.is_tracing(message)) st0
     2.9                  else
    2.10 -                  (st0 /: Isar_Document.message_positions(command, message))(
    2.11 +                  (st0 /: Isabelle_Document.message_positions(command, message))(
    2.12                      (st, range) => st.add_markup(Text.Info(range, result)))
    2.13 -              val st2 = (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
    2.14 +              val st2 = (st1 /: Isabelle_Document.message_reports(message))(_ accumulate _)
    2.15                st2
    2.16              case _ => System.err.println("Ignored message without serial number: " + message); this
    2.17            }
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/PIDE/isabelle_document.ML	Tue Nov 29 20:18:02 2011 +0100
     3.3 @@ -0,0 +1,84 @@
     3.4 +(*  Title:      Pure/PIDE/isabelle_document.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Protocol message formats for interactive Isar documents.
     3.8 +*)
     3.9 +
    3.10 +structure Isabelle_Document: sig end =
    3.11 +struct
    3.12 +
    3.13 +val _ =
    3.14 +  Isabelle_Process.add_command "Isabelle_Document.define_command"
    3.15 +    (fn [id, name, text] =>
    3.16 +      Document.change_state (Document.define_command (Document.parse_id id) name text));
    3.17 +
    3.18 +val _ =
    3.19 +  Isabelle_Process.add_command "Isabelle_Document.cancel_execution"
    3.20 +    (fn [] => ignore (Document.cancel_execution (Document.state ())));
    3.21 +
    3.22 +val _ =
    3.23 +  Isabelle_Process.add_command "Isabelle_Document.update_perspective"
    3.24 +    (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
    3.25 +      let
    3.26 +        val old_id = Document.parse_id old_id_string;
    3.27 +        val new_id = Document.parse_id new_id_string;
    3.28 +        val ids = YXML.parse_body ids_yxml
    3.29 +          |> let open XML.Decode in list int end;
    3.30 +
    3.31 +        val _ = Future.join_tasks (Document.cancel_execution state);
    3.32 +      in
    3.33 +        state
    3.34 +        |> Document.update_perspective old_id new_id name ids
    3.35 +        |> Document.execute new_id
    3.36 +      end));
    3.37 +
    3.38 +val _ =
    3.39 +  Isabelle_Process.add_command "Isabelle_Document.update"
    3.40 +    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    3.41 +      let
    3.42 +        val old_id = Document.parse_id old_id_string;
    3.43 +        val new_id = Document.parse_id new_id_string;
    3.44 +        val edits =
    3.45 +          YXML.parse_body edits_yxml |>
    3.46 +            let open XML.Decode in
    3.47 +              list (pair string
    3.48 +                (variant
    3.49 +                 [fn ([], []) => Document.Clear,
    3.50 +                  fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    3.51 +                  fn ([], a) =>
    3.52 +                    Document.Header
    3.53 +                      (Exn.Res
    3.54 +                        (triple (pair string string) (list string) (list (pair string bool)) a)),
    3.55 +                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
    3.56 +                  fn (a, []) => Document.Perspective (map int_atom a)]))
    3.57 +            end;
    3.58 +
    3.59 +        val running = Document.cancel_execution state;
    3.60 +        val (assignment, state1) = Document.update old_id new_id edits state;
    3.61 +        val _ = Future.join_tasks running;
    3.62 +        val _ =
    3.63 +          Output.raw_message Isabelle_Markup.assign_execs
    3.64 +            ((new_id, assignment) |>
    3.65 +              let open XML.Encode
    3.66 +              in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
    3.67 +              |> YXML.string_of_body);
    3.68 +        val state2 = Document.execute new_id state1;
    3.69 +      in state2 end));
    3.70 +
    3.71 +val _ =
    3.72 +  Isabelle_Process.add_command "Isabelle_Document.remove_versions"
    3.73 +    (fn [versions_yxml] => Document.change_state (fn state =>
    3.74 +      let
    3.75 +        val versions =
    3.76 +          YXML.parse_body versions_yxml |>
    3.77 +            let open XML.Decode in list int end;
    3.78 +        val state1 = Document.remove_versions versions state;
    3.79 +        val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml;
    3.80 +      in state1 end));
    3.81 +
    3.82 +val _ =
    3.83 +  Isabelle_Process.add_command "Isabelle_Document.invoke_scala"
    3.84 +    (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
    3.85 +
    3.86 +end;
    3.87 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/PIDE/isabelle_document.scala	Tue Nov 29 20:18:02 2011 +0100
     4.3 @@ -0,0 +1,231 @@
     4.4 +/*  Title:      Pure/PIDE/isabelle_document.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Protocol message formats for interactive Isar documents.
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +
    4.13 +object Isabelle_Document
    4.14 +{
    4.15 +  /* document editing */
    4.16 +
    4.17 +  object Assign
    4.18 +  {
    4.19 +    def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
    4.20 +      try {
    4.21 +        import XML.Decode._
    4.22 +        val body = YXML.parse_body(text)
    4.23 +        Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
    4.24 +      }
    4.25 +      catch {
    4.26 +        case ERROR(_) => None
    4.27 +        case _: XML.XML_Atom => None
    4.28 +        case _: XML.XML_Body => None
    4.29 +      }
    4.30 +  }
    4.31 +
    4.32 +  object Removed
    4.33 +  {
    4.34 +    def unapply(text: String): Option[List[Document.Version_ID]] =
    4.35 +      try {
    4.36 +        import XML.Decode._
    4.37 +        Some(list(long)(YXML.parse_body(text)))
    4.38 +      }
    4.39 +      catch {
    4.40 +        case ERROR(_) => None
    4.41 +        case _: XML.XML_Atom => None
    4.42 +        case _: XML.XML_Body => None
    4.43 +      }
    4.44 +  }
    4.45 +
    4.46 +
    4.47 +  /* toplevel transactions */
    4.48 +
    4.49 +  sealed abstract class Status
    4.50 +  case object Unprocessed extends Status
    4.51 +  case class Forked(forks: Int) extends Status
    4.52 +  case object Finished extends Status
    4.53 +  case object Failed extends Status
    4.54 +
    4.55 +  def command_status(markup: List[Markup]): Status =
    4.56 +  {
    4.57 +    val forks = (0 /: markup) {
    4.58 +      case (i, Markup(Isabelle_Markup.FORKED, _)) => i + 1
    4.59 +      case (i, Markup(Isabelle_Markup.JOINED, _)) => i - 1
    4.60 +      case (i, _) => i
    4.61 +    }
    4.62 +    if (forks != 0) Forked(forks)
    4.63 +    else if (markup.exists(_.name == Isabelle_Markup.FAILED)) Failed
    4.64 +    else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished
    4.65 +    else Unprocessed
    4.66 +  }
    4.67 +
    4.68 +  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
    4.69 +  {
    4.70 +    def total: Int = unprocessed + running + finished + failed
    4.71 +  }
    4.72 +
    4.73 +  def node_status(
    4.74 +    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
    4.75 +  {
    4.76 +    var unprocessed = 0
    4.77 +    var running = 0
    4.78 +    var finished = 0
    4.79 +    var failed = 0
    4.80 +    node.commands.foreach(command =>
    4.81 +      command_status(state.command_state(version, command).status) match {
    4.82 +        case Unprocessed => unprocessed += 1
    4.83 +        case Forked(_) => running += 1
    4.84 +        case Finished => finished += 1
    4.85 +        case Failed => failed += 1
    4.86 +      })
    4.87 +    Node_Status(unprocessed, running, finished, failed)
    4.88 +  }
    4.89 +
    4.90 +
    4.91 +  /* result messages */
    4.92 +
    4.93 +  def clean_message(body: XML.Body): XML.Body =
    4.94 +    body filter { case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false case _ => true } map
    4.95 +      { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
    4.96 +
    4.97 +  def message_reports(msg: XML.Tree): List[XML.Elem] =
    4.98 +    msg match {
    4.99 +      case elem @ XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => List(elem)
   4.100 +      case XML.Elem(_, body) => body.flatMap(message_reports)
   4.101 +      case XML.Text(_) => Nil
   4.102 +    }
   4.103 +
   4.104 +
   4.105 +  /* specific messages */
   4.106 +
   4.107 +  def is_ready(msg: XML.Tree): Boolean =
   4.108 +    msg match {
   4.109 +      case XML.Elem(Markup(Isabelle_Markup.STATUS, _),
   4.110 +        List(XML.Elem(Markup(Isabelle_Markup.READY, _), _))) => true
   4.111 +      case _ => false
   4.112 +    }
   4.113 +
   4.114 + def is_tracing(msg: XML.Tree): Boolean =
   4.115 +    msg match {
   4.116 +      case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
   4.117 +      case _ => false
   4.118 +    }
   4.119 +
   4.120 +  def is_warning(msg: XML.Tree): Boolean =
   4.121 +    msg match {
   4.122 +      case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
   4.123 +      case _ => false
   4.124 +    }
   4.125 +
   4.126 +  def is_error(msg: XML.Tree): Boolean =
   4.127 +    msg match {
   4.128 +      case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
   4.129 +      case _ => false
   4.130 +    }
   4.131 +
   4.132 +  def is_state(msg: XML.Tree): Boolean =
   4.133 +    msg match {
   4.134 +      case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
   4.135 +        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
   4.136 +      case _ => false
   4.137 +    }
   4.138 +
   4.139 +
   4.140 +  /* reported positions */
   4.141 +
   4.142 +  private val include_pos =
   4.143 +    Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT,
   4.144 +      Isabelle_Markup.POSITION)
   4.145 +
   4.146 +  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   4.147 +  {
   4.148 +    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
   4.149 +      tree match {
   4.150 +        case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
   4.151 +        if include_pos(name) && id == command.id =>
   4.152 +          val range = command.decode(raw_range).restrict(command.range)
   4.153 +          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
   4.154 +        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
   4.155 +        case _ => set
   4.156 +      }
   4.157 +    val set = positions(Set.empty, message)
   4.158 +    if (set.isEmpty && !is_state(message))
   4.159 +      set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
   4.160 +    else set
   4.161 +  }
   4.162 +}
   4.163 +
   4.164 +
   4.165 +trait Isabelle_Document extends Isabelle_Process
   4.166 +{
   4.167 +  /* commands */
   4.168 +
   4.169 +  def define_command(command: Command): Unit =
   4.170 +    input("Isabelle_Document.define_command",
   4.171 +      Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
   4.172 +
   4.173 +
   4.174 +  /* document versions */
   4.175 +
   4.176 +  def cancel_execution()
   4.177 +  {
   4.178 +    input("Isabelle_Document.cancel_execution")
   4.179 +  }
   4.180 +
   4.181 +  def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
   4.182 +    name: Document.Node.Name, perspective: Command.Perspective)
   4.183 +  {
   4.184 +    val ids =
   4.185 +    { import XML.Encode._
   4.186 +      list(long)(perspective.commands.map(_.id)) }
   4.187 +
   4.188 +    input("Isabelle_Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
   4.189 +      name.node, YXML.string_of_body(ids))
   4.190 +  }
   4.191 +
   4.192 +  def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
   4.193 +    edits: List[Document.Edit_Command])
   4.194 +  {
   4.195 +    val edits_yxml =
   4.196 +    { import XML.Encode._
   4.197 +      def id: T[Command] = (cmd => long(cmd.id))
   4.198 +      def encode_edit(dir: String)
   4.199 +          : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
   4.200 +        variant(List(
   4.201 +          { case Document.Node.Clear() => (Nil, Nil) },
   4.202 +          { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
   4.203 +          { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
   4.204 +              (Nil,
   4.205 +                triple(pair(string, string), list(string), list(pair(string, bool)))(
   4.206 +                  (dir, a), b, c)) },
   4.207 +          { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
   4.208 +          { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
   4.209 +      def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
   4.210 +      {
   4.211 +        val (name, edit) = node_edit
   4.212 +        val dir = Isabelle_System.posix_path(name.dir)
   4.213 +        pair(string, encode_edit(dir))(name.node, edit)
   4.214 +      })
   4.215 +      YXML.string_of_body(encode(edits)) }
   4.216 +    input("Isabelle_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
   4.217 +  }
   4.218 +
   4.219 +  def remove_versions(versions: List[Document.Version])
   4.220 +  {
   4.221 +    val versions_yxml =
   4.222 +      { import XML.Encode._
   4.223 +        YXML.string_of_body(list(long)(versions.map(_.id))) }
   4.224 +    input("Isabelle_Document.remove_versions", versions_yxml)
   4.225 +  }
   4.226 +
   4.227 +
   4.228 +  /* method invocation service */
   4.229 +
   4.230 +  def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
   4.231 +  {
   4.232 +    input("Isabelle_Document.invoke_scala", id, tag.toString, res)
   4.233 +  }
   4.234 +}
     5.1 --- a/src/Pure/PIDE/isar_document.ML	Tue Nov 29 20:17:11 2011 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,84 +0,0 @@
     5.4 -(*  Title:      Pure/PIDE/isar_document.ML
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Protocol message formats for interactive Isar documents.
     5.8 -*)
     5.9 -
    5.10 -structure Isar_Document: sig end =
    5.11 -struct
    5.12 -
    5.13 -val _ =
    5.14 -  Isabelle_Process.add_command "Isar_Document.define_command"
    5.15 -    (fn [id, name, text] =>
    5.16 -      Document.change_state (Document.define_command (Document.parse_id id) name text));
    5.17 -
    5.18 -val _ =
    5.19 -  Isabelle_Process.add_command "Isar_Document.cancel_execution"
    5.20 -    (fn [] => ignore (Document.cancel_execution (Document.state ())));
    5.21 -
    5.22 -val _ =
    5.23 -  Isabelle_Process.add_command "Isar_Document.update_perspective"
    5.24 -    (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
    5.25 -      let
    5.26 -        val old_id = Document.parse_id old_id_string;
    5.27 -        val new_id = Document.parse_id new_id_string;
    5.28 -        val ids = YXML.parse_body ids_yxml
    5.29 -          |> let open XML.Decode in list int end;
    5.30 -
    5.31 -        val _ = Future.join_tasks (Document.cancel_execution state);
    5.32 -      in
    5.33 -        state
    5.34 -        |> Document.update_perspective old_id new_id name ids
    5.35 -        |> Document.execute new_id
    5.36 -      end));
    5.37 -
    5.38 -val _ =
    5.39 -  Isabelle_Process.add_command "Isar_Document.update"
    5.40 -    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    5.41 -      let
    5.42 -        val old_id = Document.parse_id old_id_string;
    5.43 -        val new_id = Document.parse_id new_id_string;
    5.44 -        val edits =
    5.45 -          YXML.parse_body edits_yxml |>
    5.46 -            let open XML.Decode in
    5.47 -              list (pair string
    5.48 -                (variant
    5.49 -                 [fn ([], []) => Document.Clear,
    5.50 -                  fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    5.51 -                  fn ([], a) =>
    5.52 -                    Document.Header
    5.53 -                      (Exn.Res
    5.54 -                        (triple (pair string string) (list string) (list (pair string bool)) a)),
    5.55 -                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
    5.56 -                  fn (a, []) => Document.Perspective (map int_atom a)]))
    5.57 -            end;
    5.58 -
    5.59 -        val running = Document.cancel_execution state;
    5.60 -        val (assignment, state1) = Document.update old_id new_id edits state;
    5.61 -        val _ = Future.join_tasks running;
    5.62 -        val _ =
    5.63 -          Output.raw_message Isabelle_Markup.assign_execs
    5.64 -            ((new_id, assignment) |>
    5.65 -              let open XML.Encode
    5.66 -              in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
    5.67 -              |> YXML.string_of_body);
    5.68 -        val state2 = Document.execute new_id state1;
    5.69 -      in state2 end));
    5.70 -
    5.71 -val _ =
    5.72 -  Isabelle_Process.add_command "Isar_Document.remove_versions"
    5.73 -    (fn [versions_yxml] => Document.change_state (fn state =>
    5.74 -      let
    5.75 -        val versions =
    5.76 -          YXML.parse_body versions_yxml |>
    5.77 -            let open XML.Decode in list int end;
    5.78 -        val state1 = Document.remove_versions versions state;
    5.79 -        val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml;
    5.80 -      in state1 end));
    5.81 -
    5.82 -val _ =
    5.83 -  Isabelle_Process.add_command "Isar_Document.invoke_scala"
    5.84 -    (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
    5.85 -
    5.86 -end;
    5.87 -
     6.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Nov 29 20:17:11 2011 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,231 +0,0 @@
     6.4 -/*  Title:      Pure/PIDE/isar_document.scala
     6.5 -    Author:     Makarius
     6.6 -
     6.7 -Protocol message formats for interactive Isar documents.
     6.8 -*/
     6.9 -
    6.10 -package isabelle
    6.11 -
    6.12 -
    6.13 -object Isar_Document
    6.14 -{
    6.15 -  /* document editing */
    6.16 -
    6.17 -  object Assign
    6.18 -  {
    6.19 -    def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
    6.20 -      try {
    6.21 -        import XML.Decode._
    6.22 -        val body = YXML.parse_body(text)
    6.23 -        Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
    6.24 -      }
    6.25 -      catch {
    6.26 -        case ERROR(_) => None
    6.27 -        case _: XML.XML_Atom => None
    6.28 -        case _: XML.XML_Body => None
    6.29 -      }
    6.30 -  }
    6.31 -
    6.32 -  object Removed
    6.33 -  {
    6.34 -    def unapply(text: String): Option[List[Document.Version_ID]] =
    6.35 -      try {
    6.36 -        import XML.Decode._
    6.37 -        Some(list(long)(YXML.parse_body(text)))
    6.38 -      }
    6.39 -      catch {
    6.40 -        case ERROR(_) => None
    6.41 -        case _: XML.XML_Atom => None
    6.42 -        case _: XML.XML_Body => None
    6.43 -      }
    6.44 -  }
    6.45 -
    6.46 -
    6.47 -  /* toplevel transactions */
    6.48 -
    6.49 -  sealed abstract class Status
    6.50 -  case object Unprocessed extends Status
    6.51 -  case class Forked(forks: Int) extends Status
    6.52 -  case object Finished extends Status
    6.53 -  case object Failed extends Status
    6.54 -
    6.55 -  def command_status(markup: List[Markup]): Status =
    6.56 -  {
    6.57 -    val forks = (0 /: markup) {
    6.58 -      case (i, Markup(Isabelle_Markup.FORKED, _)) => i + 1
    6.59 -      case (i, Markup(Isabelle_Markup.JOINED, _)) => i - 1
    6.60 -      case (i, _) => i
    6.61 -    }
    6.62 -    if (forks != 0) Forked(forks)
    6.63 -    else if (markup.exists(_.name == Isabelle_Markup.FAILED)) Failed
    6.64 -    else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished
    6.65 -    else Unprocessed
    6.66 -  }
    6.67 -
    6.68 -  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
    6.69 -  {
    6.70 -    def total: Int = unprocessed + running + finished + failed
    6.71 -  }
    6.72 -
    6.73 -  def node_status(
    6.74 -    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
    6.75 -  {
    6.76 -    var unprocessed = 0
    6.77 -    var running = 0
    6.78 -    var finished = 0
    6.79 -    var failed = 0
    6.80 -    node.commands.foreach(command =>
    6.81 -      command_status(state.command_state(version, command).status) match {
    6.82 -        case Unprocessed => unprocessed += 1
    6.83 -        case Forked(_) => running += 1
    6.84 -        case Finished => finished += 1
    6.85 -        case Failed => failed += 1
    6.86 -      })
    6.87 -    Node_Status(unprocessed, running, finished, failed)
    6.88 -  }
    6.89 -
    6.90 -
    6.91 -  /* result messages */
    6.92 -
    6.93 -  def clean_message(body: XML.Body): XML.Body =
    6.94 -    body filter { case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false case _ => true } map
    6.95 -      { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
    6.96 -
    6.97 -  def message_reports(msg: XML.Tree): List[XML.Elem] =
    6.98 -    msg match {
    6.99 -      case elem @ XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => List(elem)
   6.100 -      case XML.Elem(_, body) => body.flatMap(message_reports)
   6.101 -      case XML.Text(_) => Nil
   6.102 -    }
   6.103 -
   6.104 -
   6.105 -  /* specific messages */
   6.106 -
   6.107 -  def is_ready(msg: XML.Tree): Boolean =
   6.108 -    msg match {
   6.109 -      case XML.Elem(Markup(Isabelle_Markup.STATUS, _),
   6.110 -        List(XML.Elem(Markup(Isabelle_Markup.READY, _), _))) => true
   6.111 -      case _ => false
   6.112 -    }
   6.113 -
   6.114 - def is_tracing(msg: XML.Tree): Boolean =
   6.115 -    msg match {
   6.116 -      case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
   6.117 -      case _ => false
   6.118 -    }
   6.119 -
   6.120 -  def is_warning(msg: XML.Tree): Boolean =
   6.121 -    msg match {
   6.122 -      case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
   6.123 -      case _ => false
   6.124 -    }
   6.125 -
   6.126 -  def is_error(msg: XML.Tree): Boolean =
   6.127 -    msg match {
   6.128 -      case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
   6.129 -      case _ => false
   6.130 -    }
   6.131 -
   6.132 -  def is_state(msg: XML.Tree): Boolean =
   6.133 -    msg match {
   6.134 -      case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
   6.135 -        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
   6.136 -      case _ => false
   6.137 -    }
   6.138 -
   6.139 -
   6.140 -  /* reported positions */
   6.141 -
   6.142 -  private val include_pos =
   6.143 -    Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT,
   6.144 -      Isabelle_Markup.POSITION)
   6.145 -
   6.146 -  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   6.147 -  {
   6.148 -    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
   6.149 -      tree match {
   6.150 -        case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
   6.151 -        if include_pos(name) && id == command.id =>
   6.152 -          val range = command.decode(raw_range).restrict(command.range)
   6.153 -          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
   6.154 -        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
   6.155 -        case _ => set
   6.156 -      }
   6.157 -    val set = positions(Set.empty, message)
   6.158 -    if (set.isEmpty && !is_state(message))
   6.159 -      set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
   6.160 -    else set
   6.161 -  }
   6.162 -}
   6.163 -
   6.164 -
   6.165 -trait Isar_Document extends Isabelle_Process
   6.166 -{
   6.167 -  /* commands */
   6.168 -
   6.169 -  def define_command(command: Command): Unit =
   6.170 -    input("Isar_Document.define_command",
   6.171 -      Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
   6.172 -
   6.173 -
   6.174 -  /* document versions */
   6.175 -
   6.176 -  def cancel_execution()
   6.177 -  {
   6.178 -    input("Isar_Document.cancel_execution")
   6.179 -  }
   6.180 -
   6.181 -  def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
   6.182 -    name: Document.Node.Name, perspective: Command.Perspective)
   6.183 -  {
   6.184 -    val ids =
   6.185 -    { import XML.Encode._
   6.186 -      list(long)(perspective.commands.map(_.id)) }
   6.187 -
   6.188 -    input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
   6.189 -      name.node, YXML.string_of_body(ids))
   6.190 -  }
   6.191 -
   6.192 -  def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
   6.193 -    edits: List[Document.Edit_Command])
   6.194 -  {
   6.195 -    val edits_yxml =
   6.196 -    { import XML.Encode._
   6.197 -      def id: T[Command] = (cmd => long(cmd.id))
   6.198 -      def encode_edit(dir: String)
   6.199 -          : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
   6.200 -        variant(List(
   6.201 -          { case Document.Node.Clear() => (Nil, Nil) },
   6.202 -          { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
   6.203 -          { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
   6.204 -              (Nil,
   6.205 -                triple(pair(string, string), list(string), list(pair(string, bool)))(
   6.206 -                  (dir, a), b, c)) },
   6.207 -          { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
   6.208 -          { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
   6.209 -      def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
   6.210 -      {
   6.211 -        val (name, edit) = node_edit
   6.212 -        val dir = Isabelle_System.posix_path(name.dir)
   6.213 -        pair(string, encode_edit(dir))(name.node, edit)
   6.214 -      })
   6.215 -      YXML.string_of_body(encode(edits)) }
   6.216 -    input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
   6.217 -  }
   6.218 -
   6.219 -  def remove_versions(versions: List[Document.Version])
   6.220 -  {
   6.221 -    val versions_yxml =
   6.222 -      { import XML.Encode._
   6.223 -        YXML.string_of_body(list(long)(versions.map(_.id))) }
   6.224 -    input("Isar_Document.remove_versions", versions_yxml)
   6.225 -  }
   6.226 -
   6.227 -
   6.228 -  /* method invocation service */
   6.229 -
   6.230 -  def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
   6.231 -  {
   6.232 -    input("Isar_Document.invoke_scala", id, tag.toString, res)
   6.233 -  }
   6.234 -}
     7.1 --- a/src/Pure/ROOT.ML	Tue Nov 29 20:17:11 2011 +0100
     7.2 +++ b/src/Pure/ROOT.ML	Tue Nov 29 20:18:02 2011 +0100
     7.3 @@ -270,7 +270,7 @@
     7.4  use "System/system_channel.ML";
     7.5  use "System/isabelle_process.ML";
     7.6  use "System/invoke_scala.ML";
     7.7 -use "PIDE/isar_document.ML";
     7.8 +use "PIDE/isabelle_document.ML";
     7.9  use "System/isar.ML";
    7.10  
    7.11  
     8.1 --- a/src/Pure/System/isabelle_process.scala	Tue Nov 29 20:17:11 2011 +0100
     8.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Nov 29 20:18:02 2011 +0100
     8.3 @@ -58,7 +58,7 @@
     8.4      def is_status = kind == Isabelle_Markup.STATUS
     8.5      def is_report = kind == Isabelle_Markup.REPORT
     8.6      def is_raw = kind == Isabelle_Markup.RAW
     8.7 -    def is_ready = Isar_Document.is_ready(message)
     8.8 +    def is_ready = Isabelle_Document.is_ready(message)
     8.9      def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
    8.10  
    8.11      override def toString: String =
    8.12 @@ -100,7 +100,7 @@
    8.13      if (kind == Isabelle_Markup.RAW)
    8.14        receiver(new Result(XML.Elem(Markup(kind, props), body)))
    8.15      else {
    8.16 -      val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    8.17 +      val msg = XML.Elem(Markup(kind, props), Isabelle_Document.clean_message(body))
    8.18        receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
    8.19      }
    8.20    }
     9.1 --- a/src/Pure/System/session.scala	Tue Nov 29 20:17:11 2011 +0100
     9.2 +++ b/src/Pure/System/session.scala	Tue Nov 29 20:18:02 2011 +0100
     9.3 @@ -211,7 +211,7 @@
     9.4        def cancel() { timer.cancel() }
     9.5      }
     9.6  
     9.7 -    var prover: Option[Isabelle_Process with Isar_Document] = None
     9.8 +    var prover: Option[Isabelle_Process with Isabelle_Document] = None
     9.9  
    9.10  
    9.11      /* delayed command changes */
    9.12 @@ -365,7 +365,7 @@
    9.13            }
    9.14          case Isabelle_Markup.Assign_Execs if result.is_raw =>
    9.15            XML.content(result.body).mkString match {
    9.16 -            case Isar_Document.Assign(id, assign) =>
    9.17 +            case Isabelle_Document.Assign(id, assign) =>
    9.18                try { handle_assign(id, assign) }
    9.19                catch { case _: Document.State.Fail => bad_result(result) }
    9.20              case _ => bad_result(result)
    9.21 @@ -378,7 +378,7 @@
    9.22            }
    9.23          case Isabelle_Markup.Removed_Versions if result.is_raw =>
    9.24            XML.content(result.body).mkString match {
    9.25 -            case Isar_Document.Removed(removed) =>
    9.26 +            case Isabelle_Document.Removed(removed) =>
    9.27                try { handle_removed(removed) }
    9.28                catch { case _: Document.State.Fail => bad_result(result) }
    9.29              case _ => bad_result(result)
    9.30 @@ -430,7 +430,7 @@
    9.31            if (phase == Session.Inactive || phase == Session.Failed) {
    9.32              phase = Session.Startup
    9.33              prover =
    9.34 -              Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Isar_Document)
    9.35 +              Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Isabelle_Document)
    9.36            }
    9.37  
    9.38          case Stop =>
    10.1 --- a/src/Pure/build-jars	Tue Nov 29 20:17:11 2011 +0100
    10.2 +++ b/src/Pure/build-jars	Tue Nov 29 20:18:02 2011 +0100
    10.3 @@ -30,8 +30,8 @@
    10.4    PIDE/blob.scala
    10.5    PIDE/command.scala
    10.6    PIDE/document.scala
    10.7 +  PIDE/isabelle_document.scala
    10.8    PIDE/isabelle_markup.scala
    10.9 -  PIDE/isar_document.scala
   10.10    PIDE/markup.scala
   10.11    PIDE/markup_tree.scala
   10.12    PIDE/text.scala
    11.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue Nov 29 20:17:11 2011 +0100
    11.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue Nov 29 20:18:02 2011 +0100
    11.3 @@ -60,7 +60,7 @@
    11.4              snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
    11.5                Markup_Tree.Select[Hyperlink](
    11.6                  {
    11.7 -                  // FIXME Isar_Document.Hyperlink extractor
    11.8 +                  // FIXME Isabelle_Document.Hyperlink extractor
    11.9                    case Text.Info(info_range,
   11.10                        XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
   11.11                      if (props.find(
    12.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Nov 29 20:17:11 2011 +0100
    12.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Nov 29 20:18:02 2011 +0100
    12.3 @@ -61,9 +61,9 @@
    12.4      val state = snapshot.command_state(command)
    12.5      if (snapshot.is_outdated) Some(outdated_color)
    12.6      else
    12.7 -      Isar_Document.command_status(state.status) match {
    12.8 -        case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
    12.9 -        case Isar_Document.Unprocessed => Some(unprocessed1_color)
   12.10 +      Isabelle_Document.command_status(state.status) match {
   12.11 +        case Isabelle_Document.Forked(i) if i > 0 => Some(running1_color)
   12.12 +        case Isabelle_Document.Unprocessed => Some(unprocessed1_color)
   12.13          case _ => None
   12.14        }
   12.15    }
   12.16 @@ -73,13 +73,13 @@
   12.17      val state = snapshot.command_state(command)
   12.18      if (snapshot.is_outdated) None
   12.19      else
   12.20 -      Isar_Document.command_status(state.status) match {
   12.21 -        case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None
   12.22 -        case Isar_Document.Unprocessed => Some(unprocessed_color)
   12.23 -        case Isar_Document.Failed => Some(error_color)
   12.24 -        case Isar_Document.Finished =>
   12.25 -          if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
   12.26 -          else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
   12.27 +      Isabelle_Document.command_status(state.status) match {
   12.28 +        case Isabelle_Document.Forked(i) => if (i > 0) Some(running_color) else None
   12.29 +        case Isabelle_Document.Unprocessed => Some(unprocessed_color)
   12.30 +        case Isabelle_Document.Failed => Some(error_color)
   12.31 +        case Isabelle_Document.Finished =>
   12.32 +          if (state.results.exists(r => Isabelle_Document.is_error(r._2))) Some(error_color)
   12.33 +          else if (state.results.exists(r => Isabelle_Document.is_warning(r._2))) Some(warning_color)
   12.34            else None
   12.35        }
   12.36    }
    13.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Tue Nov 29 20:17:11 2011 +0100
    13.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Nov 29 20:18:02 2011 +0100
    13.3 @@ -94,7 +94,7 @@
    13.4  
    13.5    /* component state -- owned by Swing thread */
    13.6  
    13.7 -  private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
    13.8 +  private var nodes_status: Map[Document.Node.Name, Isabelle_Document.Node_Status] = Map.empty
    13.9  
   13.10    private object Node_Renderer_Component extends Label
   13.11    {
   13.12 @@ -152,7 +152,7 @@
   13.13        for {
   13.14          name <- nodes
   13.15          node <- snapshot.version.nodes.get(name)
   13.16 -        val status = Isar_Document.node_status(snapshot.state, snapshot.version, node)
   13.17 +        val status = Isabelle_Document.node_status(snapshot.state, snapshot.version, node)
   13.18        } nodes_status1 += (name -> status)
   13.19  
   13.20        if (nodes_status != nodes_status1) {