merged
authorwenzelm
Tue Aug 12 20:42:39 2014 +0200 (2014-08-12)
changeset 57919a2a7c1de4752
parent 57898 f7f75b33d6c8
parent 57918 f5d73caba4e5
child 57920 c1953856cfca
merged
src/Pure/GUI/jfx_thread.scala
src/Pure/System/isabelle_font.scala
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Aug 12 17:18:12 2014 +0200
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Aug 12 20:42:39 2014 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4    is_some (Keyword.command_keyword name) andalso
     1.5      let
     1.6        val markup =
     1.7 -        Outer_Syntax.scan Position.none name
     1.8 +        Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none name
     1.9          |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
    1.10          |> map (snd o fst);
    1.11        val _ = Context_Position.reports ctxt (map (pair pos) markup);
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 12 17:18:12 2014 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 12 20:42:39 2014 +0200
     2.3 @@ -525,7 +525,7 @@
     2.4      fun do_method named_thms ctxt =
     2.5        let
     2.6          val ref_of_str =
     2.7 -          suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
     2.8 +          suffix ";" #> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none #> Parse_Spec.xthm
     2.9            #> fst
    2.10          val thms = named_thms |> maps snd
    2.11          val facts = named_thms |> map (ref_of_str o fst o fst)
    2.12 @@ -551,7 +551,7 @@
    2.13            let
    2.14              val (type_encs, lam_trans) =
    2.15                !meth
    2.16 -              |> Outer_Syntax.scan Position.start
    2.17 +              |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
    2.18                |> filter Token.is_proper |> tl
    2.19                |> Metis_Tactic.parse_metis_options |> fst
    2.20                |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
     3.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 12 17:18:12 2014 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 12 20:42:39 2014 +0200
     3.3 @@ -221,7 +221,7 @@
     3.4  
     3.5      val thy = Proof_Context.theory_of lthy
     3.6      val dummy_thm = Thm.transfer thy Drule.dummy_thm
     3.7 -    val pointer = Outer_Syntax.scan Position.none bundle_name
     3.8 +    val pointer = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none bundle_name
     3.9      val restore_lifting_att = 
    3.10        ([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer])
    3.11    in
     4.1 --- a/src/HOL/Tools/try0.ML	Tue Aug 12 17:18:12 2014 +0200
     4.2 +++ b/src/HOL/Tools/try0.ML	Tue Aug 12 20:42:39 2014 +0200
     4.3 @@ -48,12 +48,12 @@
     4.4        NONE
     4.5    end;
     4.6  
     4.7 -val parse_method =
     4.8 -  enclose "(" ")"
     4.9 -  #> Outer_Syntax.scan Position.start
    4.10 -  #> filter Token.is_proper
    4.11 -  #> Scan.read Token.stopper Method.parse
    4.12 -  #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
    4.13 +fun parse_method s =
    4.14 +  enclose "(" ")" s
    4.15 +  |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
    4.16 +  |> filter Token.is_proper
    4.17 +  |> Scan.read Token.stopper Method.parse
    4.18 +  |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
    4.19  
    4.20  fun apply_named_method_on_first_goal ctxt =
    4.21    parse_method
     5.1 --- a/src/Pure/Concurrent/future.scala	Tue Aug 12 17:18:12 2014 +0200
     5.2 +++ b/src/Pure/Concurrent/future.scala	Tue Aug 12 20:42:39 2014 +0200
     5.3 @@ -37,7 +37,7 @@
     5.4    def join: A
     5.5    def map[B](f: A => B): Future[B] = Future.fork { f(join) }
     5.6  
     5.7 -  override def toString =
     5.8 +  override def toString: String =
     5.9      peek match {
    5.10        case None => "<future>"
    5.11        case Some(Exn.Exn(_)) => "<failed>"
     6.1 --- a/src/Pure/GUI/gui.scala	Tue Aug 12 17:18:12 2014 +0200
     6.2 +++ b/src/Pure/GUI/gui.scala	Tue Aug 12 20:42:39 2014 +0200
     6.3 @@ -7,9 +7,10 @@
     6.4  
     6.5  package isabelle
     6.6  
     6.7 -
     6.8  import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
     6.9 -import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
    6.10 +import java.io.{FileInputStream, BufferedInputStream}
    6.11 +import java.awt.{GraphicsEnvironment, Image, Component, Container, Toolkit, Window, Font,
    6.12 +  KeyboardFocusManager}
    6.13  import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
    6.14  import java.awt.geom.AffineTransform
    6.15  import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
    6.16 @@ -232,5 +233,15 @@
    6.17      import scala.collection.JavaConversions._
    6.18      font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
    6.19    }
    6.20 +
    6.21 +  def font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
    6.22 +    new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
    6.23 +
    6.24 +  def install_fonts()
    6.25 +  {
    6.26 +    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
    6.27 +    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
    6.28 +      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
    6.29 +  }
    6.30  }
    6.31  
     7.1 --- a/src/Pure/GUI/html5_panel.scala	Tue Aug 12 17:18:12 2014 +0200
     7.2 +++ b/src/Pure/GUI/html5_panel.scala	Tue Aug 12 20:42:39 2014 +0200
     7.3 @@ -1,5 +1,5 @@
     7.4  /*  Title:      Pure/GUI/html5_panel.scala
     7.5 -    Module:     PIDE-GUI
     7.6 +    Module:     PIDE-JFX
     7.7      Author:     Makarius
     7.8  
     7.9  HTML5 panel based on Java FX WebView.
    7.10 @@ -54,7 +54,7 @@
    7.11  class HTML5_Panel extends javafx.embed.swing.JFXPanel
    7.12  {
    7.13    private val future =
    7.14 -    JFX_Thread.future {
    7.15 +    JFX_GUI.Thread.future {
    7.16        val pane = new Web_View_Workaround
    7.17  
    7.18        val web_view = pane.web_view
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/GUI/jfx_gui.scala	Tue Aug 12 20:42:39 2014 +0200
     8.3 @@ -0,0 +1,55 @@
     8.4 +/*  Title:      Pure/GUI/jfx_thread.scala
     8.5 +    Module:     PIDE-JFX
     8.6 +    Author:     Makarius
     8.7 +
     8.8 +Basic GUI tools (for Java FX).
     8.9 +*/
    8.10 +
    8.11 +package isabelle
    8.12 +
    8.13 +
    8.14 +import java.io.{FileInputStream, BufferedInputStream}
    8.15 +
    8.16 +import javafx.application.{Platform => JFX_Platform}
    8.17 +import javafx.scene.text.{Font => JFX_Font}
    8.18 +
    8.19 +
    8.20 +object JFX_GUI
    8.21 +{
    8.22 +  /* evaluation within the Java FX application thread */
    8.23 +
    8.24 +  object Thread
    8.25 +  {
    8.26 +    def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
    8.27 +    def require() = Predef.require(JFX_Platform.isFxApplicationThread())
    8.28 +
    8.29 +    def later(body: => Unit)
    8.30 +    {
    8.31 +      if (JFX_Platform.isFxApplicationThread()) body
    8.32 +      else JFX_Platform.runLater(new Runnable { def run = body })
    8.33 +    }
    8.34 +
    8.35 +    def future[A](body: => A): Future[A] =
    8.36 +    {
    8.37 +      if (JFX_Platform.isFxApplicationThread()) Future.value(body)
    8.38 +      else {
    8.39 +        val promise = Future.promise[A]
    8.40 +        later { promise.fulfill_result(Exn.capture(body)) }
    8.41 +        promise
    8.42 +      }
    8.43 +    }
    8.44 +  }
    8.45 +
    8.46 +
    8.47 +  /* Isabelle fonts */
    8.48 +
    8.49 +  def install_fonts()
    8.50 +  {
    8.51 +    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS"))) {
    8.52 +      val stream = new BufferedInputStream(new FileInputStream(font.file))
    8.53 +      try { JFX_Font.loadFont(stream, 1.0) }
    8.54 +      finally { stream.close }
    8.55 +    }
    8.56 +  }
    8.57 +
    8.58 +}
     9.1 --- a/src/Pure/GUI/jfx_thread.scala	Tue Aug 12 17:18:12 2014 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,38 +0,0 @@
     9.4 -/*  Title:      Pure/GUI/jfx_thread.scala
     9.5 -    Module:     PIDE-GUI
     9.6 -    Author:     Makarius
     9.7 -
     9.8 -Evaluation within the Java FX application thread.
     9.9 -*/
    9.10 -
    9.11 -package isabelle
    9.12 -
    9.13 -import javafx.application.{Platform => JFX_Platform}
    9.14 -
    9.15 -
    9.16 -object JFX_Thread
    9.17 -{
    9.18 -  /* checks */
    9.19 -
    9.20 -  def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
    9.21 -  def require() = Predef.require(JFX_Platform.isFxApplicationThread())
    9.22 -
    9.23 -
    9.24 -  /* asynchronous context switch */
    9.25 -
    9.26 -  def later(body: => Unit)
    9.27 -  {
    9.28 -    if (JFX_Platform.isFxApplicationThread()) body
    9.29 -    else JFX_Platform.runLater(new Runnable { def run = body })
    9.30 -  }
    9.31 -
    9.32 -  def future[A](body: => A): Future[A] =
    9.33 -  {
    9.34 -    if (JFX_Platform.isFxApplicationThread()) Future.value(body)
    9.35 -    else {
    9.36 -      val promise = Future.promise[A]
    9.37 -      later { promise.fulfill_result(Exn.capture(body)) }
    9.38 -      promise
    9.39 -    }
    9.40 -  }
    9.41 -}
    10.1 --- a/src/Pure/General/name_space.ML	Tue Aug 12 17:18:12 2014 +0200
    10.2 +++ b/src/Pure/General/name_space.ML	Tue Aug 12 20:42:39 2014 +0200
    10.3 @@ -14,7 +14,7 @@
    10.4    val kind_of: T -> string
    10.5    val defined_entry: T -> string -> bool
    10.6    val the_entry: T -> string ->
    10.7 -    {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
    10.8 +    {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
    10.9    val entry_ord: T -> string * string -> order
   10.10    val markup: T -> string -> Markup.T
   10.11    val is_concealed: T -> string -> bool
   10.12 @@ -92,10 +92,10 @@
   10.13    group: serial option,
   10.14    theory_name: string,
   10.15    pos: Position.T,
   10.16 -  id: serial};
   10.17 +  serial: serial};
   10.18  
   10.19 -fun entry_markup def kind (name, {pos, id, ...}: entry) =
   10.20 -  Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
   10.21 +fun entry_markup def kind (name, {pos, serial, ...}: entry) =
   10.22 +  Markup.properties (Position.entity_properties_of def serial pos) (Markup.entity kind name);
   10.23  
   10.24  fun print_entry_ref kind (name, entry) =
   10.25    quote (Markup.markup (entry_markup false kind (name, entry)) name);
   10.26 @@ -152,7 +152,7 @@
   10.27      NONE => error (undefined kind name)
   10.28    | SOME (_, entry) => entry);
   10.29  
   10.30 -fun entry_ord space = int_ord o pairself (#id o the_entry space);
   10.31 +fun entry_ord space = int_ord o pairself (#serial o the_entry space);
   10.32  
   10.33  fun markup (Name_Space {kind, entries, ...}) name =
   10.34    (case Change_Table.lookup entries name of
   10.35 @@ -275,7 +275,7 @@
   10.36          else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
   10.37      val entries' = (entries1, entries2) |> Change_Table.join
   10.38        (fn name => fn ((_, entry1), (_, entry2)) =>
   10.39 -        if #id entry1 = #id entry2 then raise Change_Table.SAME
   10.40 +        if #serial entry1 = #serial entry2 then raise Change_Table.SAME
   10.41          else err_dup kind' (name, entry1) (name, entry2) Position.none);
   10.42    in make_name_space (kind', internals', entries') end;
   10.43  
   10.44 @@ -448,7 +448,7 @@
   10.45        group = group,
   10.46        theory_name = theory_name,
   10.47        pos = pos,
   10.48 -      id = serial ()};
   10.49 +      serial = serial ()};
   10.50      val space' =
   10.51        space |> map_name_space (fn (kind, internals, entries) =>
   10.52          let
    11.1 --- a/src/Pure/General/position.ML	Tue Aug 12 17:18:12 2014 +0200
    11.2 +++ b/src/Pure/General/position.ML	Tue Aug 12 20:42:39 2014 +0200
    11.3 @@ -153,9 +153,9 @@
    11.4  
    11.5  val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
    11.6  
    11.7 -fun entity_properties_of def id pos =
    11.8 -  if def then (Markup.defN, Markup.print_int id) :: properties_of pos
    11.9 -  else (Markup.refN, Markup.print_int id) :: def_properties_of pos;
   11.10 +fun entity_properties_of def serial pos =
   11.11 +  if def then (Markup.defN, Markup.print_int serial) :: properties_of pos
   11.12 +  else (Markup.refN, Markup.print_int serial) :: def_properties_of pos;
   11.13  
   11.14  fun default_properties default props =
   11.15    if exists (member (op =) Markup.position_properties o #1) props then props
    12.1 --- a/src/Pure/General/position.scala	Tue Aug 12 17:18:12 2014 +0200
    12.2 +++ b/src/Pure/General/position.scala	Tue Aug 12 20:42:39 2014 +0200
    12.3 @@ -54,7 +54,7 @@
    12.4  
    12.5    object Range
    12.6    {
    12.7 -    def apply(range: Symbol.Range): T = Offset(range.start) ::: Offset(range.stop)
    12.8 +    def apply(range: Symbol.Range): T = Offset(range.start) ::: End_Offset(range.stop)
    12.9      def unapply(pos: T): Option[Symbol.Range] =
   12.10        (pos, pos) match {
   12.11          case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
   12.12 @@ -81,17 +81,17 @@
   12.13        }
   12.14    }
   12.15  
   12.16 -  object Reported
   12.17 +  object Identified
   12.18    {
   12.19 -    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name, Symbol.Range)] =
   12.20 -      (pos, pos) match {
   12.21 -        case (Id(id), Range(range)) =>
   12.22 +    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =
   12.23 +      pos match {
   12.24 +        case Id(id) =>
   12.25            val chunk_name =
   12.26              pos match {
   12.27                case File(name) => Symbol.Text_Chunk.File(name)
   12.28                case _ => Symbol.Text_Chunk.Default
   12.29              }
   12.30 -          Some((id, chunk_name, range))
   12.31 +          Some((id, chunk_name))
   12.32          case _ => None
   12.33        }
   12.34    }
    13.1 --- a/src/Pure/General/properties.scala	Tue Aug 12 17:18:12 2014 +0200
    13.2 +++ b/src/Pure/General/properties.scala	Tue Aug 12 20:42:39 2014 +0200
    13.3 @@ -27,7 +27,7 @@
    13.4  
    13.5      object Int
    13.6      {
    13.7 -      def apply(x: scala.Int): java.lang.String = x.toString
    13.8 +      def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
    13.9        def unapply(s: java.lang.String): Option[scala.Int] =
   13.10          try { Some(Integer.parseInt(s)) }
   13.11          catch { case _: NumberFormatException => None }
   13.12 @@ -35,7 +35,7 @@
   13.13  
   13.14      object Long
   13.15      {
   13.16 -      def apply(x: scala.Long): java.lang.String = x.toString
   13.17 +      def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
   13.18        def unapply(s: java.lang.String): Option[scala.Long] =
   13.19          try { Some(java.lang.Long.parseLong(s)) }
   13.20          catch { case _: NumberFormatException => None }
    14.1 --- a/src/Pure/General/time.scala	Tue Aug 12 17:18:12 2014 +0200
    14.2 +++ b/src/Pure/General/time.scala	Tue Aug 12 20:42:39 2014 +0200
    14.3 @@ -40,7 +40,7 @@
    14.4    def is_zero: Boolean = ms == 0
    14.5    def is_relevant: Boolean = ms >= 1
    14.6  
    14.7 -  override def toString = Time.print_seconds(seconds)
    14.8 +  override def toString: String = Time.print_seconds(seconds)
    14.9  
   14.10    def message: String = toString + "s"
   14.11  }
    15.1 --- a/src/Pure/General/timing.scala	Tue Aug 12 17:18:12 2014 +0200
    15.2 +++ b/src/Pure/General/timing.scala	Tue Aug 12 20:42:39 2014 +0200
    15.3 @@ -38,6 +38,6 @@
    15.4    def message: String =
    15.5      elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
    15.6  
    15.7 -  override def toString = message
    15.8 +  override def toString: String = message
    15.9  }
   15.10  
    16.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Aug 12 17:18:12 2014 +0200
    16.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 12 20:42:39 2014 +0200
    16.3 @@ -744,7 +744,7 @@
    16.4  val _ =
    16.5    Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command"
    16.6      (props_text :|-- (fn (pos, str) =>
    16.7 -      (case Outer_Syntax.parse pos str of
    16.8 +      (case Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos str of
    16.9          [tr] => Scan.succeed (K tr)
   16.10        | _ => Scan.fail_with (K (fn () => "exactly one command expected")))
   16.11        handle ERROR msg => Scan.fail_with (K (fn () => msg))));
    17.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Aug 12 17:18:12 2014 +0200
    17.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 12 20:42:39 2014 +0200
    17.3 @@ -31,8 +31,10 @@
    17.4      (local_theory -> Proof.state) parser -> unit
    17.5    val help_outer_syntax: string list -> unit
    17.6    val print_outer_syntax: unit -> unit
    17.7 -  val scan: Position.T -> string -> Token.T list
    17.8 -  val parse: Position.T -> string -> Toplevel.transition list
    17.9 +  val scan: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
   17.10 +  val parse: (Scan.lexicon * Scan.lexicon) * outer_syntax ->
   17.11 +    Position.T -> string -> Toplevel.transition list
   17.12 +  val parse_spans: Token.T list -> Command_Span.span list
   17.13    type isar
   17.14    val isar: TextIO.instream -> bool -> isar
   17.15    val side_comments: Token.T list -> Token.T list
   17.16 @@ -256,18 +258,49 @@
   17.17  
   17.18  (* off-line scanning/parsing *)
   17.19  
   17.20 -fun scan pos str =
   17.21 +fun scan lexs pos =
   17.22 +  Source.of_string #>
   17.23 +  Symbol.source #>
   17.24 +  Token.source {do_recover = SOME false} (K lexs) pos #>
   17.25 +  Source.exhaust;
   17.26 +
   17.27 +fun parse (lexs, syntax) pos str =
   17.28    Source.of_string str
   17.29    |> Symbol.source
   17.30 -  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   17.31 +  |> Token.source {do_recover = SOME false} (K lexs) pos
   17.32 +  |> toplevel_source false NONE (K (lookup_commands syntax))
   17.33    |> Source.exhaust;
   17.34  
   17.35 -fun parse pos str =
   17.36 -  Source.of_string str
   17.37 -  |> Symbol.source
   17.38 -  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   17.39 -  |> toplevel_source false NONE lookup_commands_dynamic
   17.40 -  |> Source.exhaust;
   17.41 +
   17.42 +(* parse spans *)
   17.43 +
   17.44 +local
   17.45 +
   17.46 +fun ship span =
   17.47 +  let
   17.48 +    val kind =
   17.49 +      if not (null span) andalso Token.is_command (hd span) andalso not (exists Token.is_error span)
   17.50 +      then Command_Span.Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
   17.51 +      else if forall Token.is_improper span then Command_Span.Ignored_Span
   17.52 +      else Command_Span.Malformed_Span;
   17.53 +  in cons (Command_Span.Span (kind, span)) end;
   17.54 +
   17.55 +fun flush (result, content, improper) =
   17.56 +  result
   17.57 +  |> not (null content) ? ship (rev content)
   17.58 +  |> not (null improper) ? ship (rev improper);
   17.59 +
   17.60 +fun parse tok (result, content, improper) =
   17.61 +  if Token.is_command tok then (flush (result, content, improper), [tok], [])
   17.62 +  else if Token.is_improper tok then (result, content, tok :: improper)
   17.63 +  else (result, tok :: (improper @ content), []);
   17.64 +
   17.65 +in
   17.66 +
   17.67 +fun parse_spans toks =
   17.68 +  fold parse toks ([], [], []) |> flush |> rev;
   17.69 +
   17.70 +end;
   17.71  
   17.72  
   17.73  (* interactive source of toplevel transformers *)
    18.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 17:18:12 2014 +0200
    18.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 20:42:39 2014 +0200
    18.3 @@ -57,8 +57,8 @@
    18.4    def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
    18.5    def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
    18.6  
    18.7 -  def load(span: List[Token]): Option[List[String]] =
    18.8 -    keywords.get(Command.name(span)) match {
    18.9 +  def load_command(name: String): Option[List[String]] =
   18.10 +    keywords.get(name) match {
   18.11        case Some((Keyword.THY_LOAD, exts)) => Some(exts)
   18.12        case _ => None
   18.13      }
   18.14 @@ -124,18 +124,16 @@
   18.15  
   18.16    /* token language */
   18.17  
   18.18 -  def scan(input: Reader[Char]): List[Token] =
   18.19 +  def scan(input: CharSequence): List[Token] =
   18.20    {
   18.21 +    var in: Reader[Char] = new CharSequenceReader(input)
   18.22      Token.Parsers.parseAll(
   18.23 -        Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match {
   18.24 +        Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), in) match {
   18.25        case Token.Parsers.Success(tokens, _) => tokens
   18.26 -      case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
   18.27 +      case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
   18.28      }
   18.29    }
   18.30  
   18.31 -  def scan(input: CharSequence): List[Token] =
   18.32 -    scan(new CharSequenceReader(input))
   18.33 -
   18.34    def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
   18.35    {
   18.36      var in: Reader[Char] = new CharSequenceReader(input)
   18.37 @@ -152,6 +150,47 @@
   18.38    }
   18.39  
   18.40  
   18.41 +  /* parse_spans */
   18.42 +
   18.43 +  def parse_spans(toks: List[Token]): List[Command_Span.Span] =
   18.44 +  {
   18.45 +    val result = new mutable.ListBuffer[Command_Span.Span]
   18.46 +    val content = new mutable.ListBuffer[Token]
   18.47 +    val improper = new mutable.ListBuffer[Token]
   18.48 +
   18.49 +    def ship(span: List[Token])
   18.50 +    {
   18.51 +      val kind =
   18.52 +        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) {
   18.53 +          val name = span.head.source
   18.54 +          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
   18.55 +          Command_Span.Command_Span(name, pos)
   18.56 +        }
   18.57 +        else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
   18.58 +        else Command_Span.Malformed_Span
   18.59 +      result += Command_Span.Span(kind, span)
   18.60 +    }
   18.61 +
   18.62 +    def flush()
   18.63 +    {
   18.64 +      if (!content.isEmpty) { ship(content.toList); content.clear }
   18.65 +      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
   18.66 +    }
   18.67 +
   18.68 +    for (tok <- toks) {
   18.69 +      if (tok.is_command) { flush(); content += tok }
   18.70 +      else if (tok.is_improper) improper += tok
   18.71 +      else { content ++= improper; improper.clear; content += tok }
   18.72 +    }
   18.73 +    flush()
   18.74 +
   18.75 +    result.toList
   18.76 +  }
   18.77 +
   18.78 +  def parse_spans(input: CharSequence): List[Command_Span.Span] =
   18.79 +    parse_spans(scan(input))
   18.80 +
   18.81 +
   18.82    /* language context */
   18.83  
   18.84    def set_language_context(context: Completion.Language_Context): Outer_Syntax =
    19.1 --- a/src/Pure/PIDE/command.ML	Tue Aug 12 17:18:12 2014 +0200
    19.2 +++ b/src/Pure/PIDE/command.ML	Tue Aug 12 20:42:39 2014 +0200
    19.3 @@ -121,9 +121,9 @@
    19.4    in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
    19.5  
    19.6  fun resolve_files master_dir blobs toks =
    19.7 -  (case Thy_Syntax.parse_spans toks of
    19.8 +  (case Outer_Syntax.parse_spans toks of
    19.9      [span] => span
   19.10 -      |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
   19.11 +      |> Command_Span.resolve_files (fn cmd => fn (path, pos) =>
   19.12          let
   19.13            fun make_file src_path (Exn.Res (file_node, NONE)) =
   19.14                  Exn.interruptible_capture (fn () =>
   19.15 @@ -140,7 +140,7 @@
   19.16              map2 make_file src_paths blobs
   19.17            else error ("Misalignment of inlined files" ^ Position.here pos)
   19.18          end)
   19.19 -      |> Thy_Syntax.span_content
   19.20 +      |> Command_Span.content
   19.21    | _ => toks);
   19.22  
   19.23  in
    20.1 --- a/src/Pure/PIDE/command.scala	Tue Aug 12 17:18:12 2014 +0200
    20.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 12 20:42:39 2014 +0200
    20.3 @@ -189,8 +189,7 @@
    20.4                def bad(): Unit = Output.warning("Ignored report message: " + msg)
    20.5  
    20.6                msg match {
    20.7 -                case XML.Elem(
    20.8 -                    Markup(name, atts @ Position.Reported(id, chunk_name, symbol_range)), args) =>
    20.9 +                case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) =>
   20.10  
   20.11                    val target =
   20.12                      if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
   20.13 @@ -198,8 +197,8 @@
   20.14                      else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
   20.15                      else None
   20.16  
   20.17 -                  target match {
   20.18 -                    case Some((target_name, target_chunk)) =>
   20.19 +                  (target, atts) match {
   20.20 +                    case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
   20.21                        target_chunk.incorporate(symbol_range) match {
   20.22                          case Some(range) =>
   20.23                            val props = Position.purge(atts)
   20.24 @@ -207,7 +206,7 @@
   20.25                            state.add_markup(false, target_name, info)
   20.26                          case None => bad(); state
   20.27                        }
   20.28 -                    case None =>
   20.29 +                    case _ =>
   20.30                        // silently ignore excessive reports
   20.31                        state
   20.32                    }
   20.33 @@ -232,7 +231,8 @@
   20.34                if (Protocol.is_inlined(message)) {
   20.35                  for {
   20.36                    (chunk_name, chunk) <- command.chunks.iterator
   20.37 -                  range <- Protocol.message_positions(self_id, chunk_name, chunk, message)
   20.38 +                  range <- Protocol.message_positions(
   20.39 +                    self_id, command.position, chunk_name, chunk, message)
   20.40                  } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
   20.41                }
   20.42                st
   20.43 @@ -250,39 +250,18 @@
   20.44  
   20.45    /* make commands */
   20.46  
   20.47 -  def name(span: List[Token]): String =
   20.48 -    span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
   20.49 -
   20.50 -  private def source_span(span: List[Token]): (String, List[Token]) =
   20.51 -  {
   20.52 -    val source: String =
   20.53 -      span match {
   20.54 -        case List(tok) => tok.source
   20.55 -        case _ => span.map(_.source).mkString
   20.56 -      }
   20.57 -
   20.58 -    val span1 = new mutable.ListBuffer[Token]
   20.59 -    var i = 0
   20.60 -    for (Token(kind, s) <- span) {
   20.61 -      val n = s.length
   20.62 -      val s1 = source.substring(i, i + n)
   20.63 -      span1 += Token(kind, s1)
   20.64 -      i += n
   20.65 -    }
   20.66 -    (source, span1.toList)
   20.67 -  }
   20.68 -
   20.69    def apply(
   20.70      id: Document_ID.Command,
   20.71      node_name: Document.Node.Name,
   20.72      blobs: List[Blob],
   20.73 -    span: List[Token]): Command =
   20.74 +    span: Command_Span.Span): Command =
   20.75    {
   20.76 -    val (source, span1) = source_span(span)
   20.77 +    val (source, span1) = span.compact_source
   20.78      new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
   20.79    }
   20.80  
   20.81 -  val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
   20.82 +  val empty: Command =
   20.83 +    Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
   20.84  
   20.85    def unparsed(
   20.86      id: Document_ID.Command,
   20.87 @@ -290,8 +269,8 @@
   20.88      results: Results,
   20.89      markup: Markup_Tree): Command =
   20.90    {
   20.91 -    val (source1, span) = source_span(List(Token(Token.Kind.UNPARSED, source)))
   20.92 -    new Command(id, Document.Node.Name.empty, Nil, span, source1, results, markup)
   20.93 +    val (source1, span1) = Command_Span.unparsed(source).compact_source
   20.94 +    new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
   20.95    }
   20.96  
   20.97    def unparsed(source: String): Command =
   20.98 @@ -333,25 +312,30 @@
   20.99      val id: Document_ID.Command,
  20.100      val node_name: Document.Node.Name,
  20.101      val blobs: List[Command.Blob],
  20.102 -    val span: List[Token],
  20.103 +    val span: Command_Span.Span,
  20.104      val source: String,
  20.105      val init_results: Command.Results,
  20.106      val init_markup: Markup_Tree)
  20.107  {
  20.108 +  /* name */
  20.109 +
  20.110 +  def name: String =
  20.111 +    span.kind match { case Command_Span.Command_Span(name, _) => name case _ => "" }
  20.112 +
  20.113 +  def position: Position.T =
  20.114 +    span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none }
  20.115 +
  20.116 +  override def toString: String = id + "/" + span.kind.toString
  20.117 +
  20.118 +
  20.119    /* classification */
  20.120  
  20.121 +  def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span]
  20.122 +  def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span
  20.123 +
  20.124    def is_undefined: Boolean = id == Document_ID.none
  20.125 -  val is_unparsed: Boolean = span.exists(_.is_unparsed)
  20.126 -  val is_unfinished: Boolean = span.exists(_.is_unfinished)
  20.127 -
  20.128 -  val is_ignored: Boolean = !span.exists(_.is_proper)
  20.129 -  val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error))
  20.130 -  def is_command: Boolean = !is_ignored && !is_malformed
  20.131 -
  20.132 -  def name: String = Command.name(span)
  20.133 -
  20.134 -  override def toString =
  20.135 -    id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
  20.136 +  val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
  20.137 +  val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
  20.138  
  20.139  
  20.140    /* blobs */
  20.141 @@ -379,7 +363,8 @@
  20.142    def range: Text.Range = chunk.range
  20.143  
  20.144    val proper_range: Text.Range =
  20.145 -    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
  20.146 +    Text.Range(0,
  20.147 +      (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
  20.148  
  20.149    def source(range: Text.Range): String = source.substring(range.start, range.stop)
  20.150  
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/Pure/PIDE/command_span.ML	Tue Aug 12 20:42:39 2014 +0200
    21.3 @@ -0,0 +1,70 @@
    21.4 +(*  Title:      Pure/PIDE/command_span.ML
    21.5 +    Author:     Makarius
    21.6 +
    21.7 +Syntactic representation of command spans.
    21.8 +*)
    21.9 +
   21.10 +signature COMMAND_SPAN =
   21.11 +sig
   21.12 +  datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
   21.13 +  datatype span = Span of kind * Token.T list
   21.14 +  val kind: span -> kind
   21.15 +  val content: span -> Token.T list
   21.16 +  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
   21.17 +end;
   21.18 +
   21.19 +structure Command_Span: COMMAND_SPAN =
   21.20 +struct
   21.21 +
   21.22 +datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
   21.23 +datatype span = Span of kind * Token.T list;
   21.24 +
   21.25 +fun kind (Span (k, _)) = k;
   21.26 +fun content (Span (_, toks)) = toks;
   21.27 +
   21.28 +
   21.29 +(* resolve inlined files *)
   21.30 +
   21.31 +local
   21.32 +
   21.33 +fun clean ((i1, t1) :: (i2, t2) :: toks) =
   21.34 +      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
   21.35 +      else (i1, t1) :: clean ((i2, t2) :: toks)
   21.36 +  | clean toks = toks;
   21.37 +
   21.38 +fun clean_tokens toks =
   21.39 +  ((0 upto length toks - 1) ~~ toks)
   21.40 +  |> filter (fn (_, tok) => Token.is_proper tok)
   21.41 +  |> clean;
   21.42 +
   21.43 +fun find_file ((_, tok) :: toks) =
   21.44 +      if Token.is_command tok then
   21.45 +        toks |> get_first (fn (i, tok) =>
   21.46 +          if Token.is_name tok then
   21.47 +            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
   21.48 +              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
   21.49 +          else NONE)
   21.50 +      else NONE
   21.51 +  | find_file [] = NONE;
   21.52 +
   21.53 +in
   21.54 +
   21.55 +fun resolve_files read_files span =
   21.56 +  (case span of
   21.57 +    Span (Command_Span (cmd, pos), toks) =>
   21.58 +      if Keyword.is_theory_load cmd then
   21.59 +        (case find_file (clean_tokens toks) of
   21.60 +          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
   21.61 +        | SOME (i, path) =>
   21.62 +            let
   21.63 +              val toks' = toks |> map_index (fn (j, tok) =>
   21.64 +                if i = j then Token.put_files (read_files cmd path) tok
   21.65 +                else tok);
   21.66 +            in Span (Command_Span (cmd, pos), toks') end)
   21.67 +      else span
   21.68 +  | _ => span);
   21.69 +
   21.70 +end;
   21.71 +
   21.72 +end;
   21.73 +
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/Pure/PIDE/command_span.scala	Tue Aug 12 20:42:39 2014 +0200
    22.3 @@ -0,0 +1,104 @@
    22.4 +/*  Title:      Pure/PIDE/command_span.scala
    22.5 +    Author:     Makarius
    22.6 +
    22.7 +Syntactic representation of command spans.
    22.8 +*/
    22.9 +
   22.10 +package isabelle
   22.11 +
   22.12 +
   22.13 +import scala.collection.mutable
   22.14 +
   22.15 +
   22.16 +object Command_Span
   22.17 +{
   22.18 +  sealed abstract class Kind {
   22.19 +    override def toString: String =
   22.20 +      this match {
   22.21 +        case Command_Span(name, _) => if (name != "") name else "<command>"
   22.22 +        case Ignored_Span => "<ignored>"
   22.23 +        case Malformed_Span => "<malformed>"
   22.24 +      }
   22.25 +  }
   22.26 +  case class Command_Span(name: String, pos: Position.T) extends Kind
   22.27 +  case object Ignored_Span extends Kind
   22.28 +  case object Malformed_Span extends Kind
   22.29 +
   22.30 +  sealed case class Span(kind: Kind, content: List[Token])
   22.31 +  {
   22.32 +    def compact_source: (String, Span) =
   22.33 +    {
   22.34 +      val source: String =
   22.35 +        content match {
   22.36 +          case List(tok) => tok.source
   22.37 +          case toks => toks.map(_.source).mkString
   22.38 +        }
   22.39 +
   22.40 +      val content1 = new mutable.ListBuffer[Token]
   22.41 +      var i = 0
   22.42 +      for (Token(kind, s) <- content) {
   22.43 +        val n = s.length
   22.44 +        val s1 = source.substring(i, i + n)
   22.45 +        content1 += Token(kind, s1)
   22.46 +        i += n
   22.47 +      }
   22.48 +      (source, Span(kind, content1.toList))
   22.49 +    }
   22.50 +  }
   22.51 +
   22.52 +  val empty: Span = Span(Ignored_Span, Nil)
   22.53 +
   22.54 +  def unparsed(source: String): Span =
   22.55 +    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
   22.56 +
   22.57 +
   22.58 +  /* resolve inlined files */
   22.59 +
   22.60 +  private def find_file(tokens: List[Token]): Option[String] =
   22.61 +  {
   22.62 +    def clean(toks: List[Token]): List[Token] =
   22.63 +      toks match {
   22.64 +        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
   22.65 +        case t :: ts => t :: clean(ts)
   22.66 +        case Nil => Nil
   22.67 +      }
   22.68 +    clean(tokens.filter(_.is_proper)) match {
   22.69 +      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
   22.70 +      case _ => None
   22.71 +    }
   22.72 +  }
   22.73 +
   22.74 +  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
   22.75 +    span.kind match {
   22.76 +      case Command_Span(name, _) =>
   22.77 +        syntax.load_command(name) match {
   22.78 +          case Some(exts) =>
   22.79 +            find_file(span.content) match {
   22.80 +              case Some(file) =>
   22.81 +                if (exts.isEmpty) List(file)
   22.82 +                else exts.map(ext => file + "." + ext)
   22.83 +              case None => Nil
   22.84 +            }
   22.85 +          case None => Nil
   22.86 +        }
   22.87 +      case _ => Nil
   22.88 +    }
   22.89 +
   22.90 +  def resolve_files(
   22.91 +      resources: Resources,
   22.92 +      syntax: Prover.Syntax,
   22.93 +      node_name: Document.Node.Name,
   22.94 +      span: Span,
   22.95 +      get_blob: Document.Node.Name => Option[Document.Blob])
   22.96 +    : List[Command.Blob] =
   22.97 +  {
   22.98 +    span_files(syntax, span).map(file_name =>
   22.99 +      Exn.capture {
  22.100 +        val name =
  22.101 +          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
  22.102 +        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
  22.103 +        (name, blob)
  22.104 +      })
  22.105 +  }
  22.106 +}
  22.107 +
    23.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 12 17:18:12 2014 +0200
    23.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 12 20:42:39 2014 +0200
    23.3 @@ -318,7 +318,7 @@
    23.4        val span =
    23.5          Lazy.lazy (fn () =>
    23.6            Position.setmp_thread_data (Position.id_only id)
    23.7 -            (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
    23.8 +            (fn () => Outer_Syntax.scan (Keyword.get_lexicons ()) (Position.id id) text) ());
    23.9        val _ =
   23.10          Position.setmp_thread_data (Position.id_only id)
   23.11            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    24.1 --- a/src/Pure/PIDE/markup_tree.scala	Tue Aug 12 17:18:12 2014 +0200
    24.2 +++ b/src/Pure/PIDE/markup_tree.scala	Tue Aug 12 20:42:39 2014 +0200
    24.3 @@ -261,7 +261,7 @@
    24.4     make_body(root_range, Nil, overlapping(root_range))
    24.5    }
    24.6  
    24.7 -  override def toString =
    24.8 +  override def toString: String =
    24.9      branches.toList.map(_._2) match {
   24.10        case Nil => "Empty"
   24.11        case list => list.mkString("Tree(", ",", ")")
    25.1 --- a/src/Pure/PIDE/protocol.scala	Tue Aug 12 17:18:12 2014 +0200
    25.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Aug 12 20:42:39 2014 +0200
    25.3 @@ -312,17 +312,21 @@
    25.4  
    25.5    def message_positions(
    25.6      self_id: Document_ID.Generic => Boolean,
    25.7 +    command_position: Position.T,
    25.8      chunk_name: Symbol.Text_Chunk.Name,
    25.9      chunk: Symbol.Text_Chunk,
   25.10      message: XML.Elem): Set[Text.Range] =
   25.11    {
   25.12      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
   25.13        props match {
   25.14 -        case Position.Reported(id, name, symbol_range)
   25.15 -        if self_id(id) && name == chunk_name =>
   25.16 -          chunk.incorporate(symbol_range) match {
   25.17 -            case Some(range) => set + range
   25.18 -            case _ => set
   25.19 +        case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
   25.20 +          Position.Range.unapply(props) orElse Position.Range.unapply(command_position) match {
   25.21 +            case Some(symbol_range) =>
   25.22 +              chunk.incorporate(symbol_range) match {
   25.23 +                case Some(range) => set + range
   25.24 +                case _ => set
   25.25 +              }
   25.26 +            case None => set
   25.27            }
   25.28          case _ => set
   25.29        }
   25.30 @@ -343,8 +347,25 @@
   25.31  }
   25.32  
   25.33  
   25.34 -trait Protocol extends Prover
   25.35 +trait Protocol
   25.36  {
   25.37 +  /* text */
   25.38 +
   25.39 +  def encode(s: String): String
   25.40 +  def decode(s: String): String
   25.41 +
   25.42 +  object Encode
   25.43 +  {
   25.44 +    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
   25.45 +  }
   25.46 +
   25.47 +
   25.48 +  /* protocol commands */
   25.49 +
   25.50 +  def protocol_command_bytes(name: String, args: Bytes*): Unit
   25.51 +  def protocol_command(name: String, args: String*): Unit
   25.52 +
   25.53 +
   25.54    /* options */
   25.55  
   25.56    def options(opts: Options): Unit =
    26.1 --- a/src/Pure/PIDE/prover.scala	Tue Aug 12 17:18:12 2014 +0200
    26.2 +++ b/src/Pure/PIDE/prover.scala	Tue Aug 12 20:42:39 2014 +0200
    26.3 @@ -1,12 +1,15 @@
    26.4  /*  Title:      Pure/PIDE/prover.scala
    26.5      Author:     Makarius
    26.6  
    26.7 -General prover operations.
    26.8 +General prover operations and process wrapping.
    26.9  */
   26.10  
   26.11  package isabelle
   26.12  
   26.13  
   26.14 +import java.io.{InputStream, OutputStream, BufferedReader, BufferedOutputStream, IOException}
   26.15 +
   26.16 +
   26.17  object Prover
   26.18  {
   26.19    /* syntax */
   26.20 @@ -14,12 +17,23 @@
   26.21    trait Syntax
   26.22    {
   26.23      def add_keywords(keywords: Thy_Header.Keywords): Syntax
   26.24 -    def scan(input: CharSequence): List[Token]
   26.25 -    def load(span: List[Token]): Option[List[String]]
   26.26 +    def parse_spans(input: CharSequence): List[Command_Span.Span]
   26.27 +    def load_command(name: String): Option[List[String]]
   26.28      def load_commands_in(text: String): Boolean
   26.29    }
   26.30  
   26.31  
   26.32 +  /* underlying system process */
   26.33 +
   26.34 +  trait System_Process
   26.35 +  {
   26.36 +    def stdout: BufferedReader
   26.37 +    def stderr: BufferedReader
   26.38 +    def terminate: Unit
   26.39 +    def join: Int
   26.40 +  }
   26.41 +
   26.42 +
   26.43    /* messages */
   26.44  
   26.45    sealed abstract class Message
   26.46 @@ -68,44 +82,287 @@
   26.47  }
   26.48  
   26.49  
   26.50 -trait Prover
   26.51 +abstract class Prover(
   26.52 +  receiver: Prover.Message => Unit,
   26.53 +  system_channel: System_Channel,
   26.54 +  system_process: Prover.System_Process) extends Protocol
   26.55  {
   26.56 -  /* text and tree data */
   26.57 +  /* output */
   26.58 +
   26.59 +  val xml_cache: XML.Cache = new XML.Cache()
   26.60 +
   26.61 +  private def system_output(text: String)
   26.62 +  {
   26.63 +    receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   26.64 +  }
   26.65 +
   26.66 +  private def protocol_output(props: Properties.T, bytes: Bytes)
   26.67 +  {
   26.68 +    receiver(new Prover.Protocol_Output(props, bytes))
   26.69 +  }
   26.70 +
   26.71 +  private def output(kind: String, props: Properties.T, body: XML.Body)
   26.72 +  {
   26.73 +    if (kind == Markup.INIT) system_channel.accepted()
   26.74  
   26.75 -  def encode(s: String): String
   26.76 -  def decode(s: String): String
   26.77 +    val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
   26.78 +    val reports = Protocol.message_reports(props, body)
   26.79 +    for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
   26.80 +  }
   26.81 +
   26.82 +  private def exit_message(rc: Int)
   26.83 +  {
   26.84 +    output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString)))
   26.85 +  }
   26.86 +
   26.87 +
   26.88  
   26.89 -  object Encode
   26.90 +  /** process manager **/
   26.91 +
   26.92 +  private val (_, process_result) =
   26.93 +    Simple_Thread.future("process_result") { system_process.join }
   26.94 +
   26.95 +  private def terminate_process()
   26.96    {
   26.97 -    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
   26.98 +    try { system_process.terminate }
   26.99 +    catch {
  26.100 +      case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
  26.101 +    }
  26.102    }
  26.103  
  26.104 -  def xml_cache: XML.Cache
  26.105 +  private val process_manager = Simple_Thread.fork("process_manager")
  26.106 +  {
  26.107 +    val (startup_failed, startup_errors) =
  26.108 +    {
  26.109 +      var finished: Option[Boolean] = None
  26.110 +      val result = new StringBuilder(100)
  26.111 +      while (finished.isEmpty && (system_process.stderr.ready || !process_result.is_finished)) {
  26.112 +        while (finished.isEmpty && system_process.stderr.ready) {
  26.113 +          try {
  26.114 +            val c = system_process.stderr.read
  26.115 +            if (c == 2) finished = Some(true)
  26.116 +            else result += c.toChar
  26.117 +          }
  26.118 +          catch { case _: IOException => finished = Some(false) }
  26.119 +        }
  26.120 +        Thread.sleep(10)
  26.121 +      }
  26.122 +      (finished.isEmpty || !finished.get, result.toString.trim)
  26.123 +    }
  26.124 +    if (startup_errors != "") system_output(startup_errors)
  26.125 +
  26.126 +    if (startup_failed) {
  26.127 +      terminate_process()
  26.128 +      process_result.join
  26.129 +      exit_message(127)
  26.130 +    }
  26.131 +    else {
  26.132 +      val (command_stream, message_stream) = system_channel.rendezvous()
  26.133 +
  26.134 +      command_input_init(command_stream)
  26.135 +      val stdout = physical_output(false)
  26.136 +      val stderr = physical_output(true)
  26.137 +      val message = message_output(message_stream)
  26.138 +
  26.139 +      val rc = process_result.join
  26.140 +      system_output("process terminated")
  26.141 +      command_input_close()
  26.142 +      for (thread <- List(stdout, stderr, message)) thread.join
  26.143 +      system_output("process_manager terminated")
  26.144 +      exit_message(rc)
  26.145 +    }
  26.146 +    system_channel.accepted()
  26.147 +  }
  26.148 +
  26.149 +
  26.150 +  /* management methods */
  26.151 +
  26.152 +  def join() { process_manager.join() }
  26.153 +
  26.154 +  def terminate()
  26.155 +  {
  26.156 +    command_input_close()
  26.157 +    system_output("Terminating prover process")
  26.158 +    terminate_process()
  26.159 +  }
  26.160 +
  26.161 +
  26.162 +
  26.163 +  /** process streams **/
  26.164 +
  26.165 +  /* command input */
  26.166 +
  26.167 +  private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
  26.168 +
  26.169 +  private def command_input_close(): Unit = command_input.foreach(_.shutdown)
  26.170 +
  26.171 +  private def command_input_init(raw_stream: OutputStream)
  26.172 +  {
  26.173 +    val name = "command_input"
  26.174 +    val stream = new BufferedOutputStream(raw_stream)
  26.175 +    command_input =
  26.176 +      Some(
  26.177 +        Consumer_Thread.fork(name)(
  26.178 +          consume =
  26.179 +            {
  26.180 +              case chunks =>
  26.181 +                try {
  26.182 +                  Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream)
  26.183 +                  chunks.foreach(_.write(stream))
  26.184 +                  stream.flush
  26.185 +                  true
  26.186 +                }
  26.187 +                catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
  26.188 +            },
  26.189 +          finish = { case () => stream.close; system_output(name + " terminated") }
  26.190 +        )
  26.191 +      )
  26.192 +  }
  26.193  
  26.194  
  26.195 -  /* process management */
  26.196 +  /* physical output */
  26.197 +
  26.198 +  private def physical_output(err: Boolean): Thread =
  26.199 +  {
  26.200 +    val (name, reader, markup) =
  26.201 +      if (err) ("standard_error", system_process.stderr, Markup.STDERR)
  26.202 +      else ("standard_output", system_process.stdout, Markup.STDOUT)
  26.203  
  26.204 -  def join(): Unit
  26.205 -  def terminate(): Unit
  26.206 -
  26.207 -  def protocol_command_bytes(name: String, args: Bytes*): Unit
  26.208 -  def protocol_command(name: String, args: String*): Unit
  26.209 +    Simple_Thread.fork(name) {
  26.210 +      try {
  26.211 +        var result = new StringBuilder(100)
  26.212 +        var finished = false
  26.213 +        while (!finished) {
  26.214 +          //{{{
  26.215 +          var c = -1
  26.216 +          var done = false
  26.217 +          while (!done && (result.length == 0 || reader.ready)) {
  26.218 +            c = reader.read
  26.219 +            if (c >= 0) result.append(c.asInstanceOf[Char])
  26.220 +            else done = true
  26.221 +          }
  26.222 +          if (result.length > 0) {
  26.223 +            output(markup, Nil, List(XML.Text(decode(result.toString))))
  26.224 +            result.length = 0
  26.225 +          }
  26.226 +          else {
  26.227 +            reader.close
  26.228 +            finished = true
  26.229 +          }
  26.230 +          //}}}
  26.231 +        }
  26.232 +      }
  26.233 +      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
  26.234 +      system_output(name + " terminated")
  26.235 +    }
  26.236 +  }
  26.237  
  26.238  
  26.239 -  /* PIDE protocol commands */
  26.240 +  /* message output */
  26.241 +
  26.242 +  private def message_output(stream: InputStream): Thread =
  26.243 +  {
  26.244 +    class EOF extends Exception
  26.245 +    class Protocol_Error(msg: String) extends Exception(msg)
  26.246 +
  26.247 +    val name = "message_output"
  26.248 +    Simple_Thread.fork(name) {
  26.249 +      val default_buffer = new Array[Byte](65536)
  26.250 +      var c = -1
  26.251  
  26.252 -  def options(opts: Options): Unit
  26.253 +      def read_int(): Int =
  26.254 +      //{{{
  26.255 +      {
  26.256 +        var n = 0
  26.257 +        c = stream.read
  26.258 +        if (c == -1) throw new EOF
  26.259 +        while (48 <= c && c <= 57) {
  26.260 +          n = 10 * n + (c - 48)
  26.261 +          c = stream.read
  26.262 +        }
  26.263 +        if (c != 10)
  26.264 +          throw new Protocol_Error("malformed header: expected integer followed by newline")
  26.265 +        else n
  26.266 +      }
  26.267 +      //}}}
  26.268  
  26.269 -  def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit
  26.270 -  def define_command(command: Command): Unit
  26.271 +      def read_chunk_bytes(): (Array[Byte], Int) =
  26.272 +      //{{{
  26.273 +      {
  26.274 +        val n = read_int()
  26.275 +        val buf =
  26.276 +          if (n <= default_buffer.size) default_buffer
  26.277 +          else new Array[Byte](n)
  26.278 +
  26.279 +        var i = 0
  26.280 +        var m = 0
  26.281 +        do {
  26.282 +          m = stream.read(buf, i, n - i)
  26.283 +          if (m != -1) i += m
  26.284 +        }
  26.285 +        while (m != -1 && n > i)
  26.286 +
  26.287 +        if (i != n)
  26.288 +          throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
  26.289 +
  26.290 +        (buf, n)
  26.291 +      }
  26.292 +      //}}}
  26.293  
  26.294 -  def discontinue_execution(): Unit
  26.295 -  def cancel_exec(id: Document_ID.Exec): Unit
  26.296 +      def read_chunk(): XML.Body =
  26.297 +      {
  26.298 +        val (buf, n) = read_chunk_bytes()
  26.299 +        YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n))
  26.300 +      }
  26.301  
  26.302 -  def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
  26.303 -    edits: List[Document.Edit_Command]): Unit
  26.304 -  def remove_versions(versions: List[Document.Version]): Unit
  26.305 +      try {
  26.306 +        do {
  26.307 +          try {
  26.308 +            val header = read_chunk()
  26.309 +            header match {
  26.310 +              case List(XML.Elem(Markup(name, props), Nil)) =>
  26.311 +                val kind = name.intern
  26.312 +                if (kind == Markup.PROTOCOL) {
  26.313 +                  val (buf, n) = read_chunk_bytes()
  26.314 +                  protocol_output(props, Bytes(buf, 0, n))
  26.315 +                }
  26.316 +                else {
  26.317 +                  val body = read_chunk()
  26.318 +                  output(kind, props, body)
  26.319 +                }
  26.320 +              case _ =>
  26.321 +                read_chunk()
  26.322 +                throw new Protocol_Error("bad header: " + header.toString)
  26.323 +            }
  26.324 +          }
  26.325 +          catch { case _: EOF => }
  26.326 +        }
  26.327 +        while (c != -1)
  26.328 +      }
  26.329 +      catch {
  26.330 +        case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
  26.331 +        case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
  26.332 +      }
  26.333 +      stream.close
  26.334  
  26.335 -  def dialog_result(serial: Long, result: String): Unit
  26.336 +      system_output(name + " terminated")
  26.337 +    }
  26.338 +  }
  26.339 +
  26.340 +
  26.341 +
  26.342 +  /** protocol commands **/
  26.343 +
  26.344 +  def protocol_command_bytes(name: String, args: Bytes*): Unit =
  26.345 +    command_input match {
  26.346 +      case Some(thread) => thread.send(Bytes(name) :: args.toList)
  26.347 +      case None => error("Uninitialized command input thread")
  26.348 +    }
  26.349 +
  26.350 +  def protocol_command(name: String, args: String*)
  26.351 +  {
  26.352 +    receiver(new Prover.Input(name, args.toList))
  26.353 +    protocol_command_bytes(name, args.map(Bytes(_)): _*)
  26.354 +  }
  26.355  }
  26.356  
    27.1 --- a/src/Pure/PIDE/resources.ML	Tue Aug 12 17:18:12 2014 +0200
    27.2 +++ b/src/Pure/PIDE/resources.ML	Tue Aug 12 20:42:39 2014 +0200
    27.3 @@ -132,7 +132,7 @@
    27.4  fun excursion master_dir last_timing init elements =
    27.5    let
    27.6      fun prepare_span span =
    27.7 -      Thy_Syntax.span_content span
    27.8 +      Command_Span.content span
    27.9        |> Command.read init master_dir []
   27.10        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
   27.11  
   27.12 @@ -157,8 +157,8 @@
   27.13      val _ = Thy_Header.define_keywords header;
   27.14  
   27.15      val lexs = Keyword.get_lexicons ();
   27.16 -    val toks = Thy_Syntax.parse_tokens lexs text_pos text;
   27.17 -    val spans = Thy_Syntax.parse_spans toks;
   27.18 +    val toks = Outer_Syntax.scan lexs text_pos text;
   27.19 +    val spans = Outer_Syntax.parse_spans toks;
   27.20      val elements = Thy_Syntax.parse_elements spans;
   27.21  
   27.22      fun init () =
    28.1 --- a/src/Pure/PIDE/resources.scala	Tue Aug 12 17:18:12 2014 +0200
    28.2 +++ b/src/Pure/PIDE/resources.scala	Tue Aug 12 20:42:39 2014 +0200
    28.3 @@ -56,8 +56,8 @@
    28.4  
    28.5    def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
    28.6      if (syntax.load_commands_in(text)) {
    28.7 -      val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    28.8 -      spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
    28.9 +      val spans = syntax.parse_spans(text)
   28.10 +      spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
   28.11      }
   28.12      else Nil
   28.13  
   28.14 @@ -126,6 +126,6 @@
   28.15    /* prover process */
   28.16  
   28.17    def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
   28.18 -    new Isabelle_Process(receiver, args) with Protocol
   28.19 +    Isabelle_Process(receiver, args)
   28.20  }
   28.21  
    29.1 --- a/src/Pure/PIDE/text.scala	Tue Aug 12 17:18:12 2014 +0200
    29.2 +++ b/src/Pure/PIDE/text.scala	Tue Aug 12 20:42:39 2014 +0200
    29.3 @@ -40,7 +40,7 @@
    29.4      if (start > stop)
    29.5        error("Bad range: [" + start.toString + ":" + stop.toString + "]")
    29.6  
    29.7 -    override def toString = "[" + start.toString + ":" + stop.toString + "]"
    29.8 +    override def toString: String = "[" + start.toString + ":" + stop.toString + "]"
    29.9  
   29.10      def length: Int = stop - start
   29.11  
   29.12 @@ -116,7 +116,7 @@
   29.13          case other: Perspective => ranges == other.ranges
   29.14          case _ => false
   29.15        }
   29.16 -    override def toString = ranges.toString
   29.17 +    override def toString: String = ranges.toString
   29.18    }
   29.19  
   29.20  
   29.21 @@ -141,7 +141,7 @@
   29.22  
   29.23    final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
   29.24    {
   29.25 -    override def toString =
   29.26 +    override def toString: String =
   29.27        (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
   29.28  
   29.29  
    30.1 --- a/src/Pure/PIDE/xml.scala	Tue Aug 12 17:18:12 2014 +0200
    30.2 +++ b/src/Pure/PIDE/xml.scala	Tue Aug 12 20:42:39 2014 +0200
    30.3 @@ -21,7 +21,7 @@
    30.4  
    30.5    type Attributes = Properties.T
    30.6  
    30.7 -  sealed abstract class Tree { override def toString = string_of_tree(this) }
    30.8 +  sealed abstract class Tree { override def toString: String = string_of_tree(this) }
    30.9    case class Elem(markup: Markup, body: List[Tree]) extends Tree
   30.10    {
   30.11      def name: String = markup.name
   30.12 @@ -150,12 +150,17 @@
   30.13      private def trim_bytes(s: String): String = new String(s.toCharArray)
   30.14  
   30.15      private def cache_string(x: String): String =
   30.16 -      lookup(x) match {
   30.17 -        case Some(y) => y
   30.18 -        case None =>
   30.19 -          val z = trim_bytes(x)
   30.20 -          if (z.length > max_string) z else store(z)
   30.21 -      }
   30.22 +      if (x == "true") "true"
   30.23 +      else if (x == "false") "false"
   30.24 +      else if (x == "0.0") "0.0"
   30.25 +      else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
   30.26 +      else
   30.27 +        lookup(x) match {
   30.28 +          case Some(y) => y
   30.29 +          case None =>
   30.30 +            val z = trim_bytes(x)
   30.31 +            if (z.length > max_string) z else store(z)
   30.32 +        }
   30.33      private def cache_props(x: Properties.T): Properties.T =
   30.34        if (x.isEmpty) x
   30.35        else
   30.36 @@ -214,9 +219,9 @@
   30.37  
   30.38      /* atomic values */
   30.39  
   30.40 -    def long_atom(i: Long): String = i.toString
   30.41 +    def long_atom(i: Long): String = Library.signed_string_of_long(i)
   30.42  
   30.43 -    def int_atom(i: Int): String = i.toString
   30.44 +    def int_atom(i: Int): String = Library.signed_string_of_int(i)
   30.45  
   30.46      def bool_atom(b: Boolean): String = if (b) "1" else "0"
   30.47  
    31.1 --- a/src/Pure/ROOT	Tue Aug 12 17:18:12 2014 +0200
    31.2 +++ b/src/Pure/ROOT	Tue Aug 12 20:42:39 2014 +0200
    31.3 @@ -160,6 +160,7 @@
    31.4      "ML/ml_syntax.ML"
    31.5      "PIDE/active.ML"
    31.6      "PIDE/command.ML"
    31.7 +    "PIDE/command_span.ML"
    31.8      "PIDE/document.ML"
    31.9      "PIDE/document_id.ML"
   31.10      "PIDE/execution.ML"
    32.1 --- a/src/Pure/ROOT.ML	Tue Aug 12 17:18:12 2014 +0200
    32.2 +++ b/src/Pure/ROOT.ML	Tue Aug 12 20:42:39 2014 +0200
    32.3 @@ -236,6 +236,7 @@
    32.4  
    32.5  (*theory sources*)
    32.6  use "Thy/thy_header.ML";
    32.7 +use "PIDE/command_span.ML";
    32.8  use "Thy/thy_syntax.ML";
    32.9  use "Thy/html.ML";
   32.10  use "Thy/latex.ML";
    33.1 --- a/src/Pure/System/isabelle_font.scala	Tue Aug 12 17:18:12 2014 +0200
    33.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.3 @@ -1,36 +0,0 @@
    33.4 -/*  Title:      Pure/System/isabelle_font.scala
    33.5 -    Author:     Makarius
    33.6 -
    33.7 -Isabelle font support.
    33.8 -*/
    33.9 -
   33.10 -package isabelle
   33.11 -
   33.12 -
   33.13 -import java.awt.{GraphicsEnvironment, Font}
   33.14 -import java.io.{FileInputStream, BufferedInputStream}
   33.15 -import javafx.scene.text.{Font => JFX_Font}
   33.16 -
   33.17 -
   33.18 -object Isabelle_Font
   33.19 -{
   33.20 -  def apply(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
   33.21 -    new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
   33.22 -
   33.23 -  def install_fonts()
   33.24 -  {
   33.25 -    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
   33.26 -    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
   33.27 -      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
   33.28 -  }
   33.29 -
   33.30 -  def install_fonts_jfx()
   33.31 -  {
   33.32 -    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS"))) {
   33.33 -      val stream = new BufferedInputStream(new FileInputStream(font.file))
   33.34 -      try { JFX_Font.loadFont(stream, 1.0) }
   33.35 -      finally { stream.close }
   33.36 -    }
   33.37 -  }
   33.38 -}
   33.39 -
    34.1 --- a/src/Pure/System/isabelle_process.ML	Tue Aug 12 17:18:12 2014 +0200
    34.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Aug 12 20:42:39 2014 +0200
    34.3 @@ -1,8 +1,7 @@
    34.4  (*  Title:      Pure/System/isabelle_process.ML
    34.5      Author:     Makarius
    34.6  
    34.7 -Isabelle process wrapper, based on private fifos for maximum
    34.8 -robustness and performance, or local socket for maximum portability.
    34.9 +Isabelle process wrapper.
   34.10  *)
   34.11  
   34.12  signature ISABELLE_PROCESS =
   34.13 @@ -108,8 +107,12 @@
   34.14      fun standard_message props name body =
   34.15        if forall (fn s => s = "") body then ()
   34.16        else
   34.17 -        message name
   34.18 -          (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
   34.19 +        let
   34.20 +          val props' =
   34.21 +            (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
   34.22 +              (false, SOME id') => props @ [(Markup.idN, id')]
   34.23 +            | _ => props);
   34.24 +        in message name props' body end;
   34.25    in
   34.26      Output.status_fn := standard_message [] Markup.statusN;
   34.27      Output.report_fn := standard_message [] Markup.reportN;
    35.1 --- a/src/Pure/System/isabelle_process.scala	Tue Aug 12 17:18:12 2014 +0200
    35.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Aug 12 20:42:39 2014 +0200
    35.3 @@ -1,318 +1,43 @@
    35.4  /*  Title:      Pure/System/isabelle_process.scala
    35.5      Author:     Makarius
    35.6 -    Options:    :folding=explicit:collapseFolds=1:
    35.7  
    35.8 -Isabelle process management -- always reactive due to multi-threaded I/O.
    35.9 +Isabelle process wrapper.
   35.10  */
   35.11  
   35.12  package isabelle
   35.13  
   35.14  
   35.15 -import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException}
   35.16 -
   35.17 -
   35.18 -class Isabelle_Process(
   35.19 -  receiver: Prover.Message => Unit = Console.println(_),
   35.20 -  prover_args: List[String] = Nil)
   35.21 +object Isabelle_Process
   35.22  {
   35.23 -  /* text and tree data */
   35.24 -
   35.25 -  def encode(s: String): String = Symbol.encode(s)
   35.26 -  def decode(s: String): String = Symbol.decode(s)
   35.27 -
   35.28 -  val xml_cache = new XML.Cache()
   35.29 -
   35.30 -
   35.31 -  /* output */
   35.32 -
   35.33 -  private def system_output(text: String)
   35.34 -  {
   35.35 -    receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   35.36 -  }
   35.37 -
   35.38 -  private def protocol_output(props: Properties.T, bytes: Bytes)
   35.39 -  {
   35.40 -    receiver(new Prover.Protocol_Output(props, bytes))
   35.41 -  }
   35.42 -
   35.43 -  private def output(kind: String, props: Properties.T, body: XML.Body)
   35.44 -  {
   35.45 -    if (kind == Markup.INIT) system_channel.accepted()
   35.46 -
   35.47 -    val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
   35.48 -    val reports = Protocol.message_reports(props, body)
   35.49 -    for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
   35.50 -  }
   35.51 -
   35.52 -  private def exit_message(rc: Int)
   35.53 -  {
   35.54 -    output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString)))
   35.55 -  }
   35.56 -
   35.57 -
   35.58 -
   35.59 -  /** process manager **/
   35.60 -
   35.61 -  def command_line(channel: System_Channel, args: List[String]): List[String] =
   35.62 -    Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: (channel.isabelle_args ::: args)
   35.63 -
   35.64 -  private val system_channel = System_Channel()
   35.65 -
   35.66 -  private val process =
   35.67 -    try {
   35.68 -      val cmdline = command_line(system_channel, prover_args)
   35.69 -      new Isabelle_System.Managed_Process(null, null, false, cmdline: _*)
   35.70 -    }
   35.71 -    catch { case e: IOException => system_channel.accepted(); throw(e) }
   35.72 -
   35.73 -  private val (_, process_result) =
   35.74 -    Simple_Thread.future("process_result") { process.join }
   35.75 -
   35.76 -  private def terminate_process()
   35.77 +  def apply(
   35.78 +    receiver: Prover.Message => Unit = Console.println(_),
   35.79 +    prover_args: List[String] = Nil): Isabelle_Process =
   35.80    {
   35.81 -    try { process.terminate }
   35.82 -    catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) }
   35.83 -  }
   35.84 -
   35.85 -  private val process_manager = Simple_Thread.fork("process_manager")
   35.86 -  {
   35.87 -    val (startup_failed, startup_errors) =
   35.88 -    {
   35.89 -      var finished: Option[Boolean] = None
   35.90 -      val result = new StringBuilder(100)
   35.91 -      while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
   35.92 -        while (finished.isEmpty && process.stderr.ready) {
   35.93 -          try {
   35.94 -            val c = process.stderr.read
   35.95 -            if (c == 2) finished = Some(true)
   35.96 -            else result += c.toChar
   35.97 -          }
   35.98 -          catch { case _: IOException => finished = Some(false) }
   35.99 -        }
  35.100 -        Thread.sleep(10)
  35.101 +    val system_channel = System_Channel()
  35.102 +    val system_process =
  35.103 +      try {
  35.104 +        val cmdline =
  35.105 +          Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
  35.106 +            (system_channel.prover_args ::: prover_args)
  35.107 +        val process =
  35.108 +          new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
  35.109 +            Prover.System_Process
  35.110 +        process.stdin.close
  35.111 +        process
  35.112        }
  35.113 -      (finished.isEmpty || !finished.get, result.toString.trim)
  35.114 -    }
  35.115 -    if (startup_errors != "") system_output(startup_errors)
  35.116 +      catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) }
  35.117  
  35.118 -    process.stdin.close
  35.119 -    if (startup_failed) {
  35.120 -      terminate_process()
  35.121 -      process_result.join
  35.122 -      exit_message(127)
  35.123 -    }
  35.124 -    else {
  35.125 -      val (command_stream, message_stream) = system_channel.rendezvous()
  35.126 -
  35.127 -      command_input_init(command_stream)
  35.128 -      val stdout = physical_output(false)
  35.129 -      val stderr = physical_output(true)
  35.130 -      val message = message_output(message_stream)
  35.131 +    new Isabelle_Process(receiver, system_channel, system_process)
  35.132 +  }
  35.133 +}
  35.134  
  35.135 -      val rc = process_result.join
  35.136 -      system_output("process terminated")
  35.137 -      command_input_close()
  35.138 -      for (thread <- List(stdout, stderr, message)) thread.join
  35.139 -      system_output("process_manager terminated")
  35.140 -      exit_message(rc)
  35.141 -    }
  35.142 -    system_channel.accepted()
  35.143 -  }
  35.144 -
  35.145 -
  35.146 -  /* management methods */
  35.147 -
  35.148 -  def join() { process_manager.join() }
  35.149 -
  35.150 -  def interrupt()
  35.151 +class Isabelle_Process private(
  35.152 +    receiver: Prover.Message => Unit,
  35.153 +    system_channel: System_Channel,
  35.154 +    system_process: Prover.System_Process)
  35.155 +  extends Prover(receiver, system_channel, system_process)
  35.156    {
  35.157 -    try { process.interrupt }
  35.158 -    catch { case e: IOException => system_output("Failed to interrupt Isabelle: " + e.getMessage) }
  35.159 -  }
  35.160 -
  35.161 -  def terminate()
  35.162 -  {
  35.163 -    command_input_close()
  35.164 -    system_output("Terminating Isabelle process")
  35.165 -    terminate_process()
  35.166 +    def encode(s: String): String = Symbol.encode(s)
  35.167 +    def decode(s: String): String = Symbol.decode(s)
  35.168    }
  35.169  
  35.170 -
  35.171 -
  35.172 -  /** process streams **/
  35.173 -
  35.174 -  /* command input */
  35.175 -
  35.176 -  private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
  35.177 -
  35.178 -  private def command_input_close(): Unit = command_input.foreach(_.shutdown)
  35.179 -
  35.180 -  private def command_input_init(raw_stream: OutputStream)
  35.181 -  {
  35.182 -    val name = "command_input"
  35.183 -    val stream = new BufferedOutputStream(raw_stream)
  35.184 -    command_input =
  35.185 -      Some(
  35.186 -        Consumer_Thread.fork(name)(
  35.187 -          consume =
  35.188 -            {
  35.189 -              case chunks =>
  35.190 -                try {
  35.191 -                  Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream)
  35.192 -                  chunks.foreach(_.write(stream))
  35.193 -                  stream.flush
  35.194 -                  true
  35.195 -                }
  35.196 -                catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
  35.197 -            },
  35.198 -          finish = { case () => stream.close; system_output(name + " terminated") }
  35.199 -        )
  35.200 -      )
  35.201 -  }
  35.202 -
  35.203 -
  35.204 -  /* physical output */
  35.205 -
  35.206 -  private def physical_output(err: Boolean): Thread =
  35.207 -  {
  35.208 -    val (name, reader, markup) =
  35.209 -      if (err) ("standard_error", process.stderr, Markup.STDERR)
  35.210 -      else ("standard_output", process.stdout, Markup.STDOUT)
  35.211 -
  35.212 -    Simple_Thread.fork(name) {
  35.213 -      try {
  35.214 -        var result = new StringBuilder(100)
  35.215 -        var finished = false
  35.216 -        while (!finished) {
  35.217 -          //{{{
  35.218 -          var c = -1
  35.219 -          var done = false
  35.220 -          while (!done && (result.length == 0 || reader.ready)) {
  35.221 -            c = reader.read
  35.222 -            if (c >= 0) result.append(c.asInstanceOf[Char])
  35.223 -            else done = true
  35.224 -          }
  35.225 -          if (result.length > 0) {
  35.226 -            output(markup, Nil, List(XML.Text(decode(result.toString))))
  35.227 -            result.length = 0
  35.228 -          }
  35.229 -          else {
  35.230 -            reader.close
  35.231 -            finished = true
  35.232 -          }
  35.233 -          //}}}
  35.234 -        }
  35.235 -      }
  35.236 -      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
  35.237 -      system_output(name + " terminated")
  35.238 -    }
  35.239 -  }
  35.240 -
  35.241 -
  35.242 -  /* message output */
  35.243 -
  35.244 -  private def message_output(stream: InputStream): Thread =
  35.245 -  {
  35.246 -    class EOF extends Exception
  35.247 -    class Protocol_Error(msg: String) extends Exception(msg)
  35.248 -
  35.249 -    val name = "message_output"
  35.250 -    Simple_Thread.fork(name) {
  35.251 -      val default_buffer = new Array[Byte](65536)
  35.252 -      var c = -1
  35.253 -
  35.254 -      def read_int(): Int =
  35.255 -      //{{{
  35.256 -      {
  35.257 -        var n = 0
  35.258 -        c = stream.read
  35.259 -        if (c == -1) throw new EOF
  35.260 -        while (48 <= c && c <= 57) {
  35.261 -          n = 10 * n + (c - 48)
  35.262 -          c = stream.read
  35.263 -        }
  35.264 -        if (c != 10)
  35.265 -          throw new Protocol_Error("malformed header: expected integer followed by newline")
  35.266 -        else n
  35.267 -      }
  35.268 -      //}}}
  35.269 -
  35.270 -      def read_chunk_bytes(): (Array[Byte], Int) =
  35.271 -      //{{{
  35.272 -      {
  35.273 -        val n = read_int()
  35.274 -        val buf =
  35.275 -          if (n <= default_buffer.size) default_buffer
  35.276 -          else new Array[Byte](n)
  35.277 -
  35.278 -        var i = 0
  35.279 -        var m = 0
  35.280 -        do {
  35.281 -          m = stream.read(buf, i, n - i)
  35.282 -          if (m != -1) i += m
  35.283 -        }
  35.284 -        while (m != -1 && n > i)
  35.285 -
  35.286 -        if (i != n)
  35.287 -          throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
  35.288 -
  35.289 -        (buf, n)
  35.290 -      }
  35.291 -      //}}}
  35.292 -
  35.293 -      def read_chunk(): XML.Body =
  35.294 -      {
  35.295 -        val (buf, n) = read_chunk_bytes()
  35.296 -        YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n))
  35.297 -      }
  35.298 -
  35.299 -      try {
  35.300 -        do {
  35.301 -          try {
  35.302 -            val header = read_chunk()
  35.303 -            header match {
  35.304 -              case List(XML.Elem(Markup(name, props), Nil)) =>
  35.305 -                val kind = name.intern
  35.306 -                if (kind == Markup.PROTOCOL) {
  35.307 -                  val (buf, n) = read_chunk_bytes()
  35.308 -                  protocol_output(props, Bytes(buf, 0, n))
  35.309 -                }
  35.310 -                else {
  35.311 -                  val body = read_chunk()
  35.312 -                  output(kind, props, body)
  35.313 -                }
  35.314 -              case _ =>
  35.315 -                read_chunk()
  35.316 -                throw new Protocol_Error("bad header: " + header.toString)
  35.317 -            }
  35.318 -          }
  35.319 -          catch { case _: EOF => }
  35.320 -        }
  35.321 -        while (c != -1)
  35.322 -      }
  35.323 -      catch {
  35.324 -        case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
  35.325 -        case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
  35.326 -      }
  35.327 -      stream.close
  35.328 -
  35.329 -      system_output(name + " terminated")
  35.330 -    }
  35.331 -  }
  35.332 -
  35.333 -
  35.334 -
  35.335 -  /** protocol commands **/
  35.336 -
  35.337 -  def protocol_command_bytes(name: String, args: Bytes*): Unit =
  35.338 -    command_input match {
  35.339 -      case Some(thread) => thread.send(Bytes(name) :: args.toList)
  35.340 -      case None => error("Uninitialized command input thread")
  35.341 -    }
  35.342 -
  35.343 -  def protocol_command(name: String, args: String*)
  35.344 -  {
  35.345 -    receiver(new Prover.Input(name, args.toList))
  35.346 -    protocol_command_bytes(name, args.map(Bytes(_)): _*)
  35.347 -  }
  35.348 -}
    36.1 --- a/src/Pure/System/system_channel.scala	Tue Aug 12 17:18:12 2014 +0200
    36.2 +++ b/src/Pure/System/system_channel.scala	Tue Aug 12 20:42:39 2014 +0200
    36.3 @@ -22,7 +22,7 @@
    36.4  abstract class System_Channel
    36.5  {
    36.6    def params: List[String]
    36.7 -  def isabelle_args: List[String]
    36.8 +  def prover_args: List[String]
    36.9    def rendezvous(): (OutputStream, InputStream)
   36.10    def accepted(): Unit
   36.11  }
   36.12 @@ -60,7 +60,7 @@
   36.13  
   36.14    def params: List[String] = List(fifo1, fifo2)
   36.15  
   36.16 -  val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
   36.17 +  val prover_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
   36.18  
   36.19    def rendezvous(): (OutputStream, InputStream) =
   36.20    {
   36.21 @@ -81,7 +81,7 @@
   36.22  
   36.23    def params: List[String] = List("127.0.0.1", server.getLocalPort.toString)
   36.24  
   36.25 -  def isabelle_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
   36.26 +  def prover_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
   36.27  
   36.28    def rendezvous(): (OutputStream, InputStream) =
   36.29    {
    37.1 --- a/src/Pure/Thy/thy_info.ML	Tue Aug 12 17:18:12 2014 +0200
    37.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Aug 12 20:42:39 2014 +0200
    37.3 @@ -380,7 +380,7 @@
    37.4  
    37.5  fun script_thy pos txt =
    37.6    let
    37.7 -    val trs = Outer_Syntax.parse pos txt;
    37.8 +    val trs = Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt;
    37.9      val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
   37.10      val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
   37.11    in Toplevel.end_theory end_pos end_state end;
    38.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    38.2 +++ b/src/Pure/Thy/thy_structure.scala	Tue Aug 12 20:42:39 2014 +0200
    38.3 @@ -0,0 +1,71 @@
    38.4 +/*  Title:      Pure/Thy/thy_structure.scala
    38.5 +    Author:     Makarius
    38.6 +
    38.7 +Nested structure of theory source.
    38.8 +*/
    38.9 +
   38.10 +package isabelle
   38.11 +
   38.12 +
   38.13 +import scala.collection.mutable
   38.14 +import scala.annotation.tailrec
   38.15 +
   38.16 +
   38.17 +object Thy_Structure
   38.18 +{
   38.19 +  sealed abstract class Entry { def length: Int }
   38.20 +  case class Block(val name: String, val body: List[Entry]) extends Entry
   38.21 +  {
   38.22 +    val length: Int = (0 /: body)(_ + _.length)
   38.23 +  }
   38.24 +  case class Atom(val command: Command) extends Entry
   38.25 +  {
   38.26 +    def length: Int = command.length
   38.27 +  }
   38.28 +
   38.29 +  def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
   38.30 +  {
   38.31 +    /* stack operations */
   38.32 +
   38.33 +    def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
   38.34 +    var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
   38.35 +      List((0, node_name.toString, buffer()))
   38.36 +
   38.37 +    @tailrec def close(level: Int => Boolean)
   38.38 +    {
   38.39 +      stack match {
   38.40 +        case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
   38.41 +          body2 += Block(name, body.toList)
   38.42 +          stack = stack.tail
   38.43 +          close(level)
   38.44 +        case _ =>
   38.45 +      }
   38.46 +    }
   38.47 +
   38.48 +    def result(): Entry =
   38.49 +    {
   38.50 +      close(_ => true)
   38.51 +      val (_, name, body) = stack.head
   38.52 +      Block(name, body.toList)
   38.53 +    }
   38.54 +
   38.55 +    def add(command: Command)
   38.56 +    {
   38.57 +      syntax.heading_level(command) match {
   38.58 +        case Some(i) =>
   38.59 +          close(_ > i)
   38.60 +          stack = (i + 1, command.source, buffer()) :: stack
   38.61 +        case None =>
   38.62 +      }
   38.63 +      stack.head._3 += Atom(command)
   38.64 +    }
   38.65 +
   38.66 +
   38.67 +    /* result structure */
   38.68 +
   38.69 +    val spans = syntax.parse_spans(text)
   38.70 +    spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
   38.71 +    result()
   38.72 +  }
   38.73 +}
   38.74 +
    39.1 --- a/src/Pure/Thy/thy_syntax.ML	Tue Aug 12 17:18:12 2014 +0200
    39.2 +++ b/src/Pure/Thy/thy_syntax.ML	Tue Aug 12 20:42:39 2014 +0200
    39.3 @@ -6,39 +6,21 @@
    39.4  
    39.5  signature THY_SYNTAX =
    39.6  sig
    39.7 -  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
    39.8    val reports_of_tokens: Token.T list -> bool * Position.report_text list
    39.9    val present_token: Token.T -> Output.output
   39.10 -  datatype span_kind = Command of string * Position.T | Ignored | Malformed
   39.11 -  datatype span = Span of span_kind * Token.T list
   39.12 -  val span_kind: span -> span_kind
   39.13 -  val span_content: span -> Token.T list
   39.14 -  val present_span: span -> Output.output
   39.15 -  val parse_spans: Token.T list -> span list
   39.16 -  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
   39.17 +  val present_span: Command_Span.span -> Output.output
   39.18    datatype 'a element = Element of 'a * ('a element list * 'a) option
   39.19    val atom: 'a -> 'a element
   39.20    val map_element: ('a -> 'b) -> 'a element -> 'b element
   39.21    val flat_element: 'a element -> 'a list
   39.22    val last_element: 'a element -> 'a
   39.23 -  val parse_elements: span list -> span element list
   39.24 +  val parse_elements: Command_Span.span list -> Command_Span.span element list
   39.25  end;
   39.26  
   39.27  structure Thy_Syntax: THY_SYNTAX =
   39.28  struct
   39.29  
   39.30 -(** tokens **)
   39.31 -
   39.32 -(* parse *)
   39.33 -
   39.34 -fun parse_tokens lexs pos =
   39.35 -  Source.of_string #>
   39.36 -  Symbol.source #>
   39.37 -  Token.source {do_recover = SOME false} (K lexs) pos #>
   39.38 -  Source.exhaust;
   39.39 -
   39.40 -
   39.41 -(* present *)
   39.42 +(** presentation **)
   39.43  
   39.44  local
   39.45  
   39.46 @@ -60,97 +42,12 @@
   39.47    let val results = map reports_of_token toks
   39.48    in (exists fst results, maps snd results) end;
   39.49  
   39.50 +end;
   39.51 +
   39.52  fun present_token tok =
   39.53    Markup.enclose (Token.markup tok) (Output.output (Token.unparse tok));
   39.54  
   39.55 -end;
   39.56 -
   39.57 -
   39.58 -
   39.59 -(** spans **)
   39.60 -
   39.61 -(* type span *)
   39.62 -
   39.63 -datatype span_kind = Command of string * Position.T | Ignored | Malformed;
   39.64 -datatype span = Span of span_kind * Token.T list;
   39.65 -
   39.66 -fun span_kind (Span (k, _)) = k;
   39.67 -fun span_content (Span (_, toks)) = toks;
   39.68 -
   39.69 -val present_span = implode o map present_token o span_content;
   39.70 -
   39.71 -
   39.72 -(* parse *)
   39.73 -
   39.74 -local
   39.75 -
   39.76 -fun make_span toks =
   39.77 -  if not (null toks) andalso Token.is_command (hd toks) then
   39.78 -    Span (Command (Token.content_of (hd toks), Token.pos_of (hd toks)), toks)
   39.79 -  else if forall Token.is_improper toks then Span (Ignored, toks)
   39.80 -  else Span (Malformed, toks);
   39.81 -
   39.82 -fun flush (result, span, improper) =
   39.83 -  result
   39.84 -  |> not (null span) ? cons (rev span)
   39.85 -  |> not (null improper) ? cons (rev improper);
   39.86 -
   39.87 -fun parse tok (result, span, improper) =
   39.88 -  if Token.is_command tok then (flush (result, span, improper), [tok], [])
   39.89 -  else if Token.is_improper tok then (result, span, tok :: improper)
   39.90 -  else (result, tok :: (improper @ span), []);
   39.91 -
   39.92 -in
   39.93 -
   39.94 -fun parse_spans toks =
   39.95 -  fold parse toks ([], [], [])
   39.96 -  |> flush |> rev |> map make_span;
   39.97 -
   39.98 -end;
   39.99 -
  39.100 -
  39.101 -(* inlined files *)
  39.102 -
  39.103 -local
  39.104 -
  39.105 -fun clean ((i1, t1) :: (i2, t2) :: toks) =
  39.106 -      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
  39.107 -      else (i1, t1) :: clean ((i2, t2) :: toks)
  39.108 -  | clean toks = toks;
  39.109 -
  39.110 -fun clean_tokens toks =
  39.111 -  ((0 upto length toks - 1) ~~ toks)
  39.112 -  |> filter (fn (_, tok) => Token.is_proper tok)
  39.113 -  |> clean;
  39.114 -
  39.115 -fun find_file ((_, tok) :: toks) =
  39.116 -      if Token.is_command tok then
  39.117 -        toks |> get_first (fn (i, tok) =>
  39.118 -          if Token.is_name tok then
  39.119 -            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
  39.120 -              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
  39.121 -          else NONE)
  39.122 -      else NONE
  39.123 -  | find_file [] = NONE;
  39.124 -
  39.125 -in
  39.126 -
  39.127 -fun resolve_files read_files span =
  39.128 -  (case span of
  39.129 -    Span (Command (cmd, pos), toks) =>
  39.130 -      if Keyword.is_theory_load cmd then
  39.131 -        (case find_file (clean_tokens toks) of
  39.132 -          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
  39.133 -        | SOME (i, path) =>
  39.134 -            let
  39.135 -              val toks' = toks |> map_index (fn (j, tok) =>
  39.136 -                if i = j then Token.put_files (read_files cmd path) tok
  39.137 -                else tok);
  39.138 -            in Span (Command (cmd, pos), toks') end)
  39.139 -      else span
  39.140 -  | _ => span);
  39.141 -
  39.142 -end;
  39.143 +val present_span = implode o map present_token o Command_Span.content;
  39.144  
  39.145  
  39.146  
  39.147 @@ -174,9 +71,9 @@
  39.148  
  39.149  (* scanning spans *)
  39.150  
  39.151 -val eof = Span (Command ("", Position.none), []);
  39.152 +val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
  39.153  
  39.154 -fun is_eof (Span (Command ("", _), _)) = true
  39.155 +fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
  39.156    | is_eof _ = false;
  39.157  
  39.158  val not_eof = not o is_eof;
  39.159 @@ -189,10 +86,13 @@
  39.160  local
  39.161  
  39.162  fun command_with pred =
  39.163 -  Scan.one (fn (Span (Command (name, _), _)) => pred name | _ => false);
  39.164 +  Scan.one
  39.165 +    (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
  39.166  
  39.167  val proof_atom =
  39.168 -  Scan.one (fn (Span (Command (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
  39.169 +  Scan.one
  39.170 +    (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => Keyword.is_proof_body name
  39.171 +      | _ => true) >> atom;
  39.172  
  39.173  fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
  39.174  and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;
    40.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 17:18:12 2014 +0200
    40.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 20:42:39 2014 +0200
    40.3 @@ -13,93 +13,6 @@
    40.4  
    40.5  object Thy_Syntax
    40.6  {
    40.7 -  /** nested structure **/
    40.8 -
    40.9 -  object Structure
   40.10 -  {
   40.11 -    sealed abstract class Entry { def length: Int }
   40.12 -    case class Block(val name: String, val body: List[Entry]) extends Entry
   40.13 -    {
   40.14 -      val length: Int = (0 /: body)(_ + _.length)
   40.15 -    }
   40.16 -    case class Atom(val command: Command) extends Entry
   40.17 -    {
   40.18 -      def length: Int = command.length
   40.19 -    }
   40.20 -
   40.21 -    def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
   40.22 -    {
   40.23 -      /* stack operations */
   40.24 -
   40.25 -      def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
   40.26 -      var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
   40.27 -        List((0, node_name.toString, buffer()))
   40.28 -
   40.29 -      @tailrec def close(level: Int => Boolean)
   40.30 -      {
   40.31 -        stack match {
   40.32 -          case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
   40.33 -            body2 += Block(name, body.toList)
   40.34 -            stack = stack.tail
   40.35 -            close(level)
   40.36 -          case _ =>
   40.37 -        }
   40.38 -      }
   40.39 -
   40.40 -      def result(): Entry =
   40.41 -      {
   40.42 -        close(_ => true)
   40.43 -        val (_, name, body) = stack.head
   40.44 -        Block(name, body.toList)
   40.45 -      }
   40.46 -
   40.47 -      def add(command: Command)
   40.48 -      {
   40.49 -        syntax.heading_level(command) match {
   40.50 -          case Some(i) =>
   40.51 -            close(_ > i)
   40.52 -            stack = (i + 1, command.source, buffer()) :: stack
   40.53 -          case None =>
   40.54 -        }
   40.55 -        stack.head._3 += Atom(command)
   40.56 -      }
   40.57 -
   40.58 -
   40.59 -      /* result structure */
   40.60 -
   40.61 -      val spans = parse_spans(syntax.scan(text))
   40.62 -      spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
   40.63 -      result()
   40.64 -    }
   40.65 -  }
   40.66 -
   40.67 -
   40.68 -
   40.69 -  /** parse spans **/
   40.70 -
   40.71 -  def parse_spans(toks: List[Token]): List[List[Token]] =
   40.72 -  {
   40.73 -    val result = new mutable.ListBuffer[List[Token]]
   40.74 -    val span = new mutable.ListBuffer[Token]
   40.75 -    val improper = new mutable.ListBuffer[Token]
   40.76 -
   40.77 -    def flush()
   40.78 -    {
   40.79 -      if (!span.isEmpty) { result += span.toList; span.clear }
   40.80 -      if (!improper.isEmpty) { result += improper.toList; improper.clear }
   40.81 -    }
   40.82 -    for (tok <- toks) {
   40.83 -      if (tok.is_command) { flush(); span += tok }
   40.84 -      else if (tok.is_improper) improper += tok
   40.85 -      else { span ++= improper; improper.clear; span += tok }
   40.86 -    }
   40.87 -    flush()
   40.88 -
   40.89 -    result.toList
   40.90 -  }
   40.91 -
   40.92 -
   40.93 -
   40.94    /** perspective **/
   40.95  
   40.96    def command_perspective(
   40.97 @@ -231,58 +144,12 @@
   40.98    }
   40.99  
  40.100  
  40.101 -  /* inlined files */
  40.102 -
  40.103 -  private def find_file(tokens: List[Token]): Option[String] =
  40.104 -  {
  40.105 -    def clean(toks: List[Token]): List[Token] =
  40.106 -      toks match {
  40.107 -        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
  40.108 -        case t :: ts => t :: clean(ts)
  40.109 -        case Nil => Nil
  40.110 -      }
  40.111 -    clean(tokens.filter(_.is_proper)) match {
  40.112 -      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
  40.113 -      case _ => None
  40.114 -    }
  40.115 -  }
  40.116 -
  40.117 -  def span_files(syntax: Prover.Syntax, span: List[Token]): List[String] =
  40.118 -    syntax.load(span) match {
  40.119 -      case Some(exts) =>
  40.120 -        find_file(span) match {
  40.121 -          case Some(file) =>
  40.122 -            if (exts.isEmpty) List(file)
  40.123 -            else exts.map(ext => file + "." + ext)
  40.124 -          case None => Nil
  40.125 -        }
  40.126 -      case None => Nil
  40.127 -    }
  40.128 -
  40.129 -  def resolve_files(
  40.130 -      resources: Resources,
  40.131 -      syntax: Prover.Syntax,
  40.132 -      node_name: Document.Node.Name,
  40.133 -      span: List[Token],
  40.134 -      get_blob: Document.Node.Name => Option[Document.Blob])
  40.135 -    : List[Command.Blob] =
  40.136 -  {
  40.137 -    span_files(syntax, span).map(file_name =>
  40.138 -      Exn.capture {
  40.139 -        val name =
  40.140 -          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
  40.141 -        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
  40.142 -        (name, blob)
  40.143 -      })
  40.144 -  }
  40.145 -
  40.146 -
  40.147    /* reparse range of command spans */
  40.148  
  40.149    @tailrec private def chop_common(
  40.150        cmds: List[Command],
  40.151 -      blobs_spans: List[(List[Command.Blob], List[Token])])
  40.152 -    : (List[Command], List[(List[Command.Blob], List[Token])]) =
  40.153 +      blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
  40.154 +    : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
  40.155    {
  40.156      (cmds, blobs_spans) match {
  40.157        case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
  40.158 @@ -301,8 +168,8 @@
  40.159    {
  40.160      val cmds0 = commands.iterator(first, last).toList
  40.161      val blobs_spans0 =
  40.162 -      parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
  40.163 -        map(span => (resolve_files(resources, syntax, name, span, get_blob), span))
  40.164 +      syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
  40.165 +        map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
  40.166  
  40.167      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
  40.168  
  40.169 @@ -337,8 +204,8 @@
  40.170      val visible = perspective.commands.toSet
  40.171  
  40.172      def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
  40.173 -      cmds.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
  40.174 -        .find(_.is_command) getOrElse cmds.last
  40.175 +      cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || visible(cmd))
  40.176 +        .find(_.is_proper) getOrElse cmds.last
  40.177  
  40.178      @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
  40.179        cmds.find(_.is_unparsed) match {
    41.1 --- a/src/Pure/Tools/find_consts.ML	Tue Aug 12 17:18:12 2014 +0200
    41.2 +++ b/src/Pure/Tools/find_consts.ML	Tue Aug 12 20:42:39 2014 +0200
    41.3 @@ -143,7 +143,7 @@
    41.4  in
    41.5  
    41.6  fun read_query pos str =
    41.7 -  Outer_Syntax.scan pos str
    41.8 +  Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
    41.9    |> filter Token.is_proper
   41.10    |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   41.11    |> #1;
    42.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Aug 12 17:18:12 2014 +0200
    42.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Aug 12 20:42:39 2014 +0200
    42.3 @@ -528,7 +528,7 @@
    42.4  in
    42.5  
    42.6  fun read_query pos str =
    42.7 -  Outer_Syntax.scan pos str
    42.8 +  Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
    42.9    |> filter Token.is_proper
   42.10    |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   42.11    |> #1;
    43.1 --- a/src/Pure/build-jars	Tue Aug 12 17:18:12 2014 +0200
    43.2 +++ b/src/Pure/build-jars	Tue Aug 12 20:42:39 2014 +0200
    43.3 @@ -20,7 +20,7 @@
    43.4    GUI/gui.scala
    43.5    GUI/gui_thread.scala
    43.6    GUI/html5_panel.scala
    43.7 -  GUI/jfx_thread.scala
    43.8 +  GUI/jfx_gui.scala
    43.9    GUI/popup.scala
   43.10    GUI/system_dialog.scala
   43.11    GUI/wrap_panel.scala
   43.12 @@ -54,6 +54,7 @@
   43.13    Isar/token.scala
   43.14    ML/ml_lex.scala
   43.15    PIDE/command.scala
   43.16 +  PIDE/command_span.scala
   43.17    PIDE/document.scala
   43.18    PIDE/document_id.scala
   43.19    PIDE/editor.scala
   43.20 @@ -71,7 +72,6 @@
   43.21    System/command_line.scala
   43.22    System/invoke_scala.scala
   43.23    System/isabelle_charset.scala
   43.24 -  System/isabelle_font.scala
   43.25    System/isabelle_process.scala
   43.26    System/isabelle_system.scala
   43.27    System/options.scala
   43.28 @@ -83,6 +83,7 @@
   43.29    Thy/present.scala
   43.30    Thy/thy_header.scala
   43.31    Thy/thy_info.scala
   43.32 +  Thy/thy_structure.scala
   43.33    Thy/thy_syntax.scala
   43.34    Tools/build.scala
   43.35    Tools/build_console.scala
    44.1 --- a/src/Pure/library.ML	Tue Aug 12 17:18:12 2014 +0200
    44.2 +++ b/src/Pure/library.ML	Tue Aug 12 20:42:39 2014 +0200
    44.3 @@ -642,14 +642,14 @@
    44.4  
    44.5  local
    44.6    val zero = ord "0";
    44.7 -  val small = 10000: int;
    44.8 -  val small_table = Vector.tabulate (small, Int.toString);
    44.9 +  val small_int = 10000: int;
   44.10 +  val small_int_table = Vector.tabulate (small_int, Int.toString);
   44.11  in
   44.12  
   44.13  fun string_of_int i =
   44.14    if i < 0 then Int.toString i
   44.15    else if i < 10 then chr (zero + i)
   44.16 -  else if i < small then Vector.sub (small_table, i)
   44.17 +  else if i < small_int then Vector.sub (small_int_table, i)
   44.18    else Int.toString i;
   44.19  
   44.20  end;
    45.1 --- a/src/Pure/library.scala	Tue Aug 12 17:18:12 2014 +0200
    45.2 +++ b/src/Pure/library.scala	Tue Aug 12 20:42:39 2014 +0200
    45.3 @@ -32,6 +32,33 @@
    45.4      error(cat_message(msg1, msg2))
    45.5  
    45.6  
    45.7 +  /* integers */
    45.8 +
    45.9 +  private val small_int = 10000
   45.10 +  private lazy val small_int_table =
   45.11 +  {
   45.12 +    val array = new Array[String](small_int)
   45.13 +    for (i <- 0 until small_int) array(i) = i.toString
   45.14 +    array
   45.15 +  }
   45.16 +
   45.17 +  def is_small_int(s: String): Boolean =
   45.18 +  {
   45.19 +    val len = s.length
   45.20 +    1 <= len && len <= 4 &&
   45.21 +    s.forall(c => '0' <= c && c <= '9') &&
   45.22 +    (len == 1 || s(0) != '0')
   45.23 +  }
   45.24 +
   45.25 +  def signed_string_of_long(i: Long): String =
   45.26 +    if (0 <= i && i < small_int) small_int_table(i.toInt)
   45.27 +    else i.toString
   45.28 +
   45.29 +  def signed_string_of_int(i: Int): String =
   45.30 +    if (0 <= i && i < small_int) small_int_table(i)
   45.31 +    else i.toString
   45.32 +
   45.33 +
   45.34    /* separated chunks */
   45.35  
   45.36    def separate[A](s: A, list: List[A]): List[A] =
    46.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 12 17:18:12 2014 +0200
    46.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 12 20:42:39 2014 +0200
    46.3 @@ -695,7 +695,7 @@
    46.4    let
    46.5      val ctxt = Proof_Context.init_global (Thy_Info.get_theory thyname);
    46.6      val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
    46.7 -      (filter Token.is_proper o Outer_Syntax.scan Position.none);
    46.8 +      (filter Token.is_proper o Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none);
    46.9    in case parse cmd_expr
   46.10     of SOME f => (writeln "Now generating code..."; f ctxt)
   46.11      | NONE => error ("Bad directive " ^ quote cmd_expr)
    47.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 12 17:18:12 2014 +0200
    47.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 12 20:42:39 2014 +0200
    47.3 @@ -24,13 +24,13 @@
    47.4  
    47.5    private case class Documentation(name: String, title: String, path: Path)
    47.6    {
    47.7 -    override def toString =
    47.8 +    override def toString: String =
    47.9        "<html><b>" + HTML.encode(name) + "</b>:  " + HTML.encode(title) + "</html>"
   47.10    }
   47.11  
   47.12    private case class Text_File(name: String, path: Path)
   47.13    {
   47.14 -    override def toString = name
   47.15 +    override def toString: String = name
   47.16    }
   47.17  
   47.18    private val root = new DefaultMutableTreeNode
    48.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Tue Aug 12 17:18:12 2014 +0200
    48.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Tue Aug 12 20:42:39 2014 +0200
    48.3 @@ -24,7 +24,7 @@
    48.4  
    48.5    private class Logic_Entry(val name: String, val description: String)
    48.6    {
    48.7 -    override def toString = description
    48.8 +    override def toString: String = description
    48.9    }
   48.10  
   48.11    def logic_selector(autosave: Boolean): Option_Component =
    49.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 12 17:18:12 2014 +0200
    49.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 12 20:42:39 2014 +0200
    49.3 @@ -21,7 +21,7 @@
    49.4  object Isabelle_Sidekick
    49.5  {
    49.6    def int_to_pos(offset: Text.Offset): Position =
    49.7 -    new Position { def getOffset = offset; override def toString = offset.toString }
    49.8 +    new Position { def getOffset = offset; override def toString: String = offset.toString }
    49.9  
   49.10    class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
   49.11    {
   49.12 @@ -39,7 +39,7 @@
   49.13      override def setStart(start: Position) = _start = start
   49.14      override def getEnd: Position = _end
   49.15      override def setEnd(end: Position) = _end = end
   49.16 -    override def toString = _name
   49.17 +    override def toString: String = _name
   49.18    }
   49.19  
   49.20    def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
   49.21 @@ -95,13 +95,11 @@
   49.22      node_name: Buffer => Option[Document.Node.Name])
   49.23    extends Isabelle_Sidekick(name)
   49.24  {
   49.25 -  import Thy_Syntax.Structure
   49.26 -
   49.27    override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   49.28    {
   49.29 -    def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
   49.30 +    def make_tree(offset: Text.Offset, entry: Thy_Structure.Entry): List[DefaultMutableTreeNode] =
   49.31        entry match {
   49.32 -        case Structure.Block(name, body) =>
   49.33 +        case Thy_Structure.Block(name, body) =>
   49.34            val node =
   49.35              new DefaultMutableTreeNode(
   49.36                new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
   49.37 @@ -111,8 +109,8 @@
   49.38                i + e.length
   49.39              })
   49.40            List(node)
   49.41 -        case Structure.Atom(command)
   49.42 -        if command.is_command && syntax.heading_level(command).isEmpty =>
   49.43 +        case Thy_Structure.Atom(command)
   49.44 +        if command.is_proper && syntax.heading_level(command).isEmpty =>
   49.45            val node =
   49.46              new DefaultMutableTreeNode(
   49.47                new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
   49.48 @@ -123,7 +121,7 @@
   49.49      node_name(buffer) match {
   49.50        case Some(name) =>
   49.51          val text = JEdit_Lib.buffer_text(buffer)
   49.52 -        val structure = Structure.parse(syntax, name, text)
   49.53 +        val structure = Thy_Structure.parse(syntax, name, text)
   49.54          make_tree(0, structure) foreach (node => data.root.add(node))
   49.55          true
   49.56        case None => false
   49.57 @@ -175,7 +173,7 @@
   49.58                    new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
   49.59                      override def getShortString: String = content
   49.60                      override def getLongString: String = info_text
   49.61 -                    override def toString = quote(content) + " " + range.toString
   49.62 +                    override def toString: String = quote(content) + " " + range.toString
   49.63                    })
   49.64                })
   49.65          }
    50.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 12 17:18:12 2014 +0200
    50.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 12 20:42:39 2014 +0200
    50.3 @@ -373,7 +373,7 @@
    50.4  
    50.5        PIDE.plugin = this
    50.6        Isabelle_System.init()
    50.7 -      Isabelle_Font.install_fonts()
    50.8 +      GUI.install_fonts()
    50.9  
   50.10        PIDE.options.update(Options.init())
   50.11        PIDE.completion_history.load()
    51.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Aug 12 17:18:12 2014 +0200
    51.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Aug 12 20:42:39 2014 +0200
    51.3 @@ -378,6 +378,8 @@
    51.4                    PIDE.editor.hyperlink_source_file(name, line, offset)
    51.5                  case Position.Def_Id_Offset(id, offset) =>
    51.6                    PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    51.7 +                case Position.Def_Id(id) =>
    51.8 +                  PIDE.editor.hyperlink_command_id(snapshot, id)
    51.9                  case _ => None
   51.10                }
   51.11              opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
   51.12 @@ -390,6 +392,8 @@
   51.13                    PIDE.editor.hyperlink_source_file(name, line, offset)
   51.14                  case Position.Id_Offset(id, offset) =>
   51.15                    PIDE.editor.hyperlink_command_id(snapshot, id, offset)
   51.16 +                case Position.Id(id) =>
   51.17 +                  PIDE.editor.hyperlink_command_id(snapshot, id)
   51.18                  case _ => None
   51.19                }
   51.20              opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    52.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Tue Aug 12 17:18:12 2014 +0200
    52.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Tue Aug 12 20:42:39 2014 +0200
    52.3 @@ -24,8 +24,8 @@
    52.4  
    52.5      font =
    52.6        Symbol.fonts.get(symbol) match {
    52.7 -        case None => Isabelle_Font(size = font_size)
    52.8 -        case Some(font_family) => Isabelle_Font(family = font_family, size = font_size)
    52.9 +        case None => GUI.font(size = font_size)
   52.10 +        case Some(font_family) => GUI.font(family = font_family, size = font_size)
   52.11        }
   52.12      action =
   52.13        Action(decoded) {