--- a/src/Doc/antiquote_setup.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Doc/antiquote_setup.ML Tue Aug 12 20:42:39 2014 +0200
@@ -208,7 +208,7 @@
is_some (Keyword.command_keyword name) andalso
let
val markup =
- Outer_Syntax.scan Position.none name
+ Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none name
|> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
|> map (snd o fst);
val _ = Context_Position.reports ctxt (map (pair pos) markup);
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 12 20:42:39 2014 +0200
@@ -525,7 +525,7 @@
fun do_method named_thms ctxt =
let
val ref_of_str =
- suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
+ suffix ";" #> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none #> Parse_Spec.xthm
#> fst
val thms = named_thms |> maps snd
val facts = named_thms |> map (ref_of_str o fst o fst)
@@ -551,7 +551,7 @@
let
val (type_encs, lam_trans) =
!meth
- |> Outer_Syntax.scan Position.start
+ |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
|> filter Token.is_proper |> tl
|> Metis_Tactic.parse_metis_options |> fst
|>> the_default [ATP_Proof_Reconstruct.partial_typesN]
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Aug 12 20:42:39 2014 +0200
@@ -221,7 +221,7 @@
val thy = Proof_Context.theory_of lthy
val dummy_thm = Thm.transfer thy Drule.dummy_thm
- val pointer = Outer_Syntax.scan Position.none bundle_name
+ val pointer = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none bundle_name
val restore_lifting_att =
([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer])
in
--- a/src/HOL/Tools/try0.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/HOL/Tools/try0.ML Tue Aug 12 20:42:39 2014 +0200
@@ -48,12 +48,12 @@
NONE
end;
-val parse_method =
- enclose "(" ")"
- #> Outer_Syntax.scan Position.start
- #> filter Token.is_proper
- #> Scan.read Token.stopper Method.parse
- #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
+fun parse_method s =
+ enclose "(" ")" s
+ |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
+ |> filter Token.is_proper
+ |> Scan.read Token.stopper Method.parse
+ |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
fun apply_named_method_on_first_goal ctxt =
parse_method
--- a/src/Pure/Concurrent/future.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/Concurrent/future.scala Tue Aug 12 20:42:39 2014 +0200
@@ -37,7 +37,7 @@
def join: A
def map[B](f: A => B): Future[B] = Future.fork { f(join) }
- override def toString =
+ override def toString: String =
peek match {
case None => "<future>"
case Some(Exn.Exn(_)) => "<failed>"
--- a/src/Pure/GUI/gui.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/GUI/gui.scala Tue Aug 12 20:42:39 2014 +0200
@@ -7,9 +7,10 @@
package isabelle
-
import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
-import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
+import java.io.{FileInputStream, BufferedInputStream}
+import java.awt.{GraphicsEnvironment, Image, Component, Container, Toolkit, Window, Font,
+ KeyboardFocusManager}
import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
import java.awt.geom.AffineTransform
import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
@@ -232,5 +233,15 @@
import scala.collection.JavaConversions._
font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
}
+
+ def font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
+ new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
+
+ def install_fonts()
+ {
+ val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
+ for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
+ ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
+ }
}
--- a/src/Pure/GUI/html5_panel.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/GUI/html5_panel.scala Tue Aug 12 20:42:39 2014 +0200
@@ -1,5 +1,5 @@
/* Title: Pure/GUI/html5_panel.scala
- Module: PIDE-GUI
+ Module: PIDE-JFX
Author: Makarius
HTML5 panel based on Java FX WebView.
@@ -54,7 +54,7 @@
class HTML5_Panel extends javafx.embed.swing.JFXPanel
{
private val future =
- JFX_Thread.future {
+ JFX_GUI.Thread.future {
val pane = new Web_View_Workaround
val web_view = pane.web_view
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/jfx_gui.scala Tue Aug 12 20:42:39 2014 +0200
@@ -0,0 +1,55 @@
+/* Title: Pure/GUI/jfx_thread.scala
+ Module: PIDE-JFX
+ Author: Makarius
+
+Basic GUI tools (for Java FX).
+*/
+
+package isabelle
+
+
+import java.io.{FileInputStream, BufferedInputStream}
+
+import javafx.application.{Platform => JFX_Platform}
+import javafx.scene.text.{Font => JFX_Font}
+
+
+object JFX_GUI
+{
+ /* evaluation within the Java FX application thread */
+
+ object Thread
+ {
+ def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
+ def require() = Predef.require(JFX_Platform.isFxApplicationThread())
+
+ def later(body: => Unit)
+ {
+ if (JFX_Platform.isFxApplicationThread()) body
+ else JFX_Platform.runLater(new Runnable { def run = body })
+ }
+
+ def future[A](body: => A): Future[A] =
+ {
+ if (JFX_Platform.isFxApplicationThread()) Future.value(body)
+ else {
+ val promise = Future.promise[A]
+ later { promise.fulfill_result(Exn.capture(body)) }
+ promise
+ }
+ }
+ }
+
+
+ /* Isabelle fonts */
+
+ def install_fonts()
+ {
+ for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS"))) {
+ val stream = new BufferedInputStream(new FileInputStream(font.file))
+ try { JFX_Font.loadFont(stream, 1.0) }
+ finally { stream.close }
+ }
+ }
+
+}
--- a/src/Pure/GUI/jfx_thread.scala Tue Aug 12 17:18:12 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-/* Title: Pure/GUI/jfx_thread.scala
- Module: PIDE-GUI
- Author: Makarius
-
-Evaluation within the Java FX application thread.
-*/
-
-package isabelle
-
-import javafx.application.{Platform => JFX_Platform}
-
-
-object JFX_Thread
-{
- /* checks */
-
- def assert() = Predef.assert(JFX_Platform.isFxApplicationThread())
- def require() = Predef.require(JFX_Platform.isFxApplicationThread())
-
-
- /* asynchronous context switch */
-
- def later(body: => Unit)
- {
- if (JFX_Platform.isFxApplicationThread()) body
- else JFX_Platform.runLater(new Runnable { def run = body })
- }
-
- def future[A](body: => A): Future[A] =
- {
- if (JFX_Platform.isFxApplicationThread()) Future.value(body)
- else {
- val promise = Future.promise[A]
- later { promise.fulfill_result(Exn.capture(body)) }
- promise
- }
- }
-}
--- a/src/Pure/General/name_space.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/General/name_space.ML Tue Aug 12 20:42:39 2014 +0200
@@ -14,7 +14,7 @@
val kind_of: T -> string
val defined_entry: T -> string -> bool
val the_entry: T -> string ->
- {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
+ {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
val entry_ord: T -> string * string -> order
val markup: T -> string -> Markup.T
val is_concealed: T -> string -> bool
@@ -92,10 +92,10 @@
group: serial option,
theory_name: string,
pos: Position.T,
- id: serial};
+ serial: serial};
-fun entry_markup def kind (name, {pos, id, ...}: entry) =
- Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
+fun entry_markup def kind (name, {pos, serial, ...}: entry) =
+ Markup.properties (Position.entity_properties_of def serial pos) (Markup.entity kind name);
fun print_entry_ref kind (name, entry) =
quote (Markup.markup (entry_markup false kind (name, entry)) name);
@@ -152,7 +152,7 @@
NONE => error (undefined kind name)
| SOME (_, entry) => entry);
-fun entry_ord space = int_ord o pairself (#id o the_entry space);
+fun entry_ord space = int_ord o pairself (#serial o the_entry space);
fun markup (Name_Space {kind, entries, ...}) name =
(case Change_Table.lookup entries name of
@@ -275,7 +275,7 @@
else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
val entries' = (entries1, entries2) |> Change_Table.join
(fn name => fn ((_, entry1), (_, entry2)) =>
- if #id entry1 = #id entry2 then raise Change_Table.SAME
+ if #serial entry1 = #serial entry2 then raise Change_Table.SAME
else err_dup kind' (name, entry1) (name, entry2) Position.none);
in make_name_space (kind', internals', entries') end;
@@ -448,7 +448,7 @@
group = group,
theory_name = theory_name,
pos = pos,
- id = serial ()};
+ serial = serial ()};
val space' =
space |> map_name_space (fn (kind, internals, entries) =>
let
--- a/src/Pure/General/position.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/General/position.ML Tue Aug 12 20:42:39 2014 +0200
@@ -153,9 +153,9 @@
val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
-fun entity_properties_of def id pos =
- if def then (Markup.defN, Markup.print_int id) :: properties_of pos
- else (Markup.refN, Markup.print_int id) :: def_properties_of pos;
+fun entity_properties_of def serial pos =
+ if def then (Markup.defN, Markup.print_int serial) :: properties_of pos
+ else (Markup.refN, Markup.print_int serial) :: def_properties_of pos;
fun default_properties default props =
if exists (member (op =) Markup.position_properties o #1) props then props
--- a/src/Pure/General/position.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/General/position.scala Tue Aug 12 20:42:39 2014 +0200
@@ -54,7 +54,7 @@
object Range
{
- def apply(range: Symbol.Range): T = Offset(range.start) ::: Offset(range.stop)
+ def apply(range: Symbol.Range): T = Offset(range.start) ::: End_Offset(range.stop)
def unapply(pos: T): Option[Symbol.Range] =
(pos, pos) match {
case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
@@ -81,17 +81,17 @@
}
}
- object Reported
+ object Identified
{
- def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name, Symbol.Range)] =
- (pos, pos) match {
- case (Id(id), Range(range)) =>
+ def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =
+ pos match {
+ case Id(id) =>
val chunk_name =
pos match {
case File(name) => Symbol.Text_Chunk.File(name)
case _ => Symbol.Text_Chunk.Default
}
- Some((id, chunk_name, range))
+ Some((id, chunk_name))
case _ => None
}
}
--- a/src/Pure/General/properties.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/General/properties.scala Tue Aug 12 20:42:39 2014 +0200
@@ -27,7 +27,7 @@
object Int
{
- def apply(x: scala.Int): java.lang.String = x.toString
+ def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
def unapply(s: java.lang.String): Option[scala.Int] =
try { Some(Integer.parseInt(s)) }
catch { case _: NumberFormatException => None }
@@ -35,7 +35,7 @@
object Long
{
- def apply(x: scala.Long): java.lang.String = x.toString
+ def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
def unapply(s: java.lang.String): Option[scala.Long] =
try { Some(java.lang.Long.parseLong(s)) }
catch { case _: NumberFormatException => None }
--- a/src/Pure/General/time.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/General/time.scala Tue Aug 12 20:42:39 2014 +0200
@@ -40,7 +40,7 @@
def is_zero: Boolean = ms == 0
def is_relevant: Boolean = ms >= 1
- override def toString = Time.print_seconds(seconds)
+ override def toString: String = Time.print_seconds(seconds)
def message: String = toString + "s"
}
--- a/src/Pure/General/timing.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/General/timing.scala Tue Aug 12 20:42:39 2014 +0200
@@ -38,6 +38,6 @@
def message: String =
elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
- override def toString = message
+ override def toString: String = message
}
--- a/src/Pure/Isar/isar_syn.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Aug 12 20:42:39 2014 +0200
@@ -744,7 +744,7 @@
val _ =
Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command"
(props_text :|-- (fn (pos, str) =>
- (case Outer_Syntax.parse pos str of
+ (case Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos str of
[tr] => Scan.succeed (K tr)
| _ => Scan.fail_with (K (fn () => "exactly one command expected")))
handle ERROR msg => Scan.fail_with (K (fn () => msg))));
--- a/src/Pure/Isar/outer_syntax.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Tue Aug 12 20:42:39 2014 +0200
@@ -31,8 +31,10 @@
(local_theory -> Proof.state) parser -> unit
val help_outer_syntax: string list -> unit
val print_outer_syntax: unit -> unit
- val scan: Position.T -> string -> Token.T list
- val parse: Position.T -> string -> Toplevel.transition list
+ val scan: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
+ val parse: (Scan.lexicon * Scan.lexicon) * outer_syntax ->
+ Position.T -> string -> Toplevel.transition list
+ val parse_spans: Token.T list -> Command_Span.span list
type isar
val isar: TextIO.instream -> bool -> isar
val side_comments: Token.T list -> Token.T list
@@ -256,18 +258,49 @@
(* off-line scanning/parsing *)
-fun scan pos str =
+fun scan lexs pos =
+ Source.of_string #>
+ Symbol.source #>
+ Token.source {do_recover = SOME false} (K lexs) pos #>
+ Source.exhaust;
+
+fun parse (lexs, syntax) pos str =
Source.of_string str
|> Symbol.source
- |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
+ |> Token.source {do_recover = SOME false} (K lexs) pos
+ |> toplevel_source false NONE (K (lookup_commands syntax))
|> Source.exhaust;
-fun parse pos str =
- Source.of_string str
- |> Symbol.source
- |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
- |> toplevel_source false NONE lookup_commands_dynamic
- |> Source.exhaust;
+
+(* parse spans *)
+
+local
+
+fun ship span =
+ let
+ val kind =
+ if not (null span) andalso Token.is_command (hd span) andalso not (exists Token.is_error span)
+ then Command_Span.Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
+ else if forall Token.is_improper span then Command_Span.Ignored_Span
+ else Command_Span.Malformed_Span;
+ in cons (Command_Span.Span (kind, span)) end;
+
+fun flush (result, content, improper) =
+ result
+ |> not (null content) ? ship (rev content)
+ |> not (null improper) ? ship (rev improper);
+
+fun parse tok (result, content, improper) =
+ if Token.is_command tok then (flush (result, content, improper), [tok], [])
+ else if Token.is_improper tok then (result, content, tok :: improper)
+ else (result, tok :: (improper @ content), []);
+
+in
+
+fun parse_spans toks =
+ fold parse toks ([], [], []) |> flush |> rev;
+
+end;
(* interactive source of toplevel transformers *)
--- a/src/Pure/Isar/outer_syntax.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Tue Aug 12 20:42:39 2014 +0200
@@ -57,8 +57,8 @@
def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
- def load(span: List[Token]): Option[List[String]] =
- keywords.get(Command.name(span)) match {
+ def load_command(name: String): Option[List[String]] =
+ keywords.get(name) match {
case Some((Keyword.THY_LOAD, exts)) => Some(exts)
case _ => None
}
@@ -124,18 +124,16 @@
/* token language */
- def scan(input: Reader[Char]): List[Token] =
+ def scan(input: CharSequence): List[Token] =
{
+ var in: Reader[Char] = new CharSequenceReader(input)
Token.Parsers.parseAll(
- Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match {
+ Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), in) match {
case Token.Parsers.Success(tokens, _) => tokens
- case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
+ case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
}
}
- def scan(input: CharSequence): List[Token] =
- scan(new CharSequenceReader(input))
-
def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
{
var in: Reader[Char] = new CharSequenceReader(input)
@@ -152,6 +150,47 @@
}
+ /* parse_spans */
+
+ def parse_spans(toks: List[Token]): List[Command_Span.Span] =
+ {
+ val result = new mutable.ListBuffer[Command_Span.Span]
+ val content = new mutable.ListBuffer[Token]
+ val improper = new mutable.ListBuffer[Token]
+
+ def ship(span: List[Token])
+ {
+ val kind =
+ if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) {
+ val name = span.head.source
+ val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
+ Command_Span.Command_Span(name, pos)
+ }
+ else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
+ else Command_Span.Malformed_Span
+ result += Command_Span.Span(kind, span)
+ }
+
+ def flush()
+ {
+ if (!content.isEmpty) { ship(content.toList); content.clear }
+ if (!improper.isEmpty) { ship(improper.toList); improper.clear }
+ }
+
+ for (tok <- toks) {
+ if (tok.is_command) { flush(); content += tok }
+ else if (tok.is_improper) improper += tok
+ else { content ++= improper; improper.clear; content += tok }
+ }
+ flush()
+
+ result.toList
+ }
+
+ def parse_spans(input: CharSequence): List[Command_Span.Span] =
+ parse_spans(scan(input))
+
+
/* language context */
def set_language_context(context: Completion.Language_Context): Outer_Syntax =
--- a/src/Pure/PIDE/command.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/PIDE/command.ML Tue Aug 12 20:42:39 2014 +0200
@@ -121,9 +121,9 @@
in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
fun resolve_files master_dir blobs toks =
- (case Thy_Syntax.parse_spans toks of
+ (case Outer_Syntax.parse_spans toks of
[span] => span
- |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
+ |> Command_Span.resolve_files (fn cmd => fn (path, pos) =>
let
fun make_file src_path (Exn.Res (file_node, NONE)) =
Exn.interruptible_capture (fn () =>
@@ -140,7 +140,7 @@
map2 make_file src_paths blobs
else error ("Misalignment of inlined files" ^ Position.here pos)
end)
- |> Thy_Syntax.span_content
+ |> Command_Span.content
| _ => toks);
in
--- a/src/Pure/PIDE/command.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/PIDE/command.scala Tue Aug 12 20:42:39 2014 +0200
@@ -189,8 +189,7 @@
def bad(): Unit = Output.warning("Ignored report message: " + msg)
msg match {
- case XML.Elem(
- Markup(name, atts @ Position.Reported(id, chunk_name, symbol_range)), args) =>
+ case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) =>
val target =
if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
@@ -198,8 +197,8 @@
else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
else None
- target match {
- case Some((target_name, target_chunk)) =>
+ (target, atts) match {
+ case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
target_chunk.incorporate(symbol_range) match {
case Some(range) =>
val props = Position.purge(atts)
@@ -207,7 +206,7 @@
state.add_markup(false, target_name, info)
case None => bad(); state
}
- case None =>
+ case _ =>
// silently ignore excessive reports
state
}
@@ -232,7 +231,8 @@
if (Protocol.is_inlined(message)) {
for {
(chunk_name, chunk) <- command.chunks.iterator
- range <- Protocol.message_positions(self_id, chunk_name, chunk, message)
+ range <- Protocol.message_positions(
+ self_id, command.position, chunk_name, chunk, message)
} st = st.add_markup(false, chunk_name, Text.Info(range, message2))
}
st
@@ -250,39 +250,18 @@
/* make commands */
- def name(span: List[Token]): String =
- span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
-
- private def source_span(span: List[Token]): (String, List[Token]) =
- {
- val source: String =
- span match {
- case List(tok) => tok.source
- case _ => span.map(_.source).mkString
- }
-
- val span1 = new mutable.ListBuffer[Token]
- var i = 0
- for (Token(kind, s) <- span) {
- val n = s.length
- val s1 = source.substring(i, i + n)
- span1 += Token(kind, s1)
- i += n
- }
- (source, span1.toList)
- }
-
def apply(
id: Document_ID.Command,
node_name: Document.Node.Name,
blobs: List[Blob],
- span: List[Token]): Command =
+ span: Command_Span.Span): Command =
{
- val (source, span1) = source_span(span)
+ val (source, span1) = span.compact_source
new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
}
- val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
+ val empty: Command =
+ Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
def unparsed(
id: Document_ID.Command,
@@ -290,8 +269,8 @@
results: Results,
markup: Markup_Tree): Command =
{
- val (source1, span) = source_span(List(Token(Token.Kind.UNPARSED, source)))
- new Command(id, Document.Node.Name.empty, Nil, span, source1, results, markup)
+ val (source1, span1) = Command_Span.unparsed(source).compact_source
+ new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
}
def unparsed(source: String): Command =
@@ -333,25 +312,30 @@
val id: Document_ID.Command,
val node_name: Document.Node.Name,
val blobs: List[Command.Blob],
- val span: List[Token],
+ val span: Command_Span.Span,
val source: String,
val init_results: Command.Results,
val init_markup: Markup_Tree)
{
+ /* name */
+
+ def name: String =
+ span.kind match { case Command_Span.Command_Span(name, _) => name case _ => "" }
+
+ def position: Position.T =
+ span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none }
+
+ override def toString: String = id + "/" + span.kind.toString
+
+
/* classification */
+ def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span]
+ def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span
+
def is_undefined: Boolean = id == Document_ID.none
- val is_unparsed: Boolean = span.exists(_.is_unparsed)
- val is_unfinished: Boolean = span.exists(_.is_unfinished)
-
- val is_ignored: Boolean = !span.exists(_.is_proper)
- val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error))
- def is_command: Boolean = !is_ignored && !is_malformed
-
- def name: String = Command.name(span)
-
- override def toString =
- id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
+ val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
+ val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
/* blobs */
@@ -379,7 +363,8 @@
def range: Text.Range = chunk.range
val proper_range: Text.Range =
- Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
+ Text.Range(0,
+ (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
def source(range: Text.Range): String = source.substring(range.start, range.stop)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/command_span.ML Tue Aug 12 20:42:39 2014 +0200
@@ -0,0 +1,70 @@
+(* Title: Pure/PIDE/command_span.ML
+ Author: Makarius
+
+Syntactic representation of command spans.
+*)
+
+signature COMMAND_SPAN =
+sig
+ datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
+ datatype span = Span of kind * Token.T list
+ val kind: span -> kind
+ val content: span -> Token.T list
+ val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
+end;
+
+structure Command_Span: COMMAND_SPAN =
+struct
+
+datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
+datatype span = Span of kind * Token.T list;
+
+fun kind (Span (k, _)) = k;
+fun content (Span (_, toks)) = toks;
+
+
+(* resolve inlined files *)
+
+local
+
+fun clean ((i1, t1) :: (i2, t2) :: toks) =
+ if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
+ else (i1, t1) :: clean ((i2, t2) :: toks)
+ | clean toks = toks;
+
+fun clean_tokens toks =
+ ((0 upto length toks - 1) ~~ toks)
+ |> filter (fn (_, tok) => Token.is_proper tok)
+ |> clean;
+
+fun find_file ((_, tok) :: toks) =
+ if Token.is_command tok then
+ toks |> get_first (fn (i, tok) =>
+ if Token.is_name tok then
+ SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
+ handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
+ else NONE)
+ else NONE
+ | find_file [] = NONE;
+
+in
+
+fun resolve_files read_files span =
+ (case span of
+ Span (Command_Span (cmd, pos), toks) =>
+ if Keyword.is_theory_load cmd then
+ (case find_file (clean_tokens toks) of
+ NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
+ | SOME (i, path) =>
+ let
+ val toks' = toks |> map_index (fn (j, tok) =>
+ if i = j then Token.put_files (read_files cmd path) tok
+ else tok);
+ in Span (Command_Span (cmd, pos), toks') end)
+ else span
+ | _ => span);
+
+end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/command_span.scala Tue Aug 12 20:42:39 2014 +0200
@@ -0,0 +1,104 @@
+/* Title: Pure/PIDE/command_span.scala
+ Author: Makarius
+
+Syntactic representation of command spans.
+*/
+
+package isabelle
+
+
+import scala.collection.mutable
+
+
+object Command_Span
+{
+ sealed abstract class Kind {
+ override def toString: String =
+ this match {
+ case Command_Span(name, _) => if (name != "") name else "<command>"
+ case Ignored_Span => "<ignored>"
+ case Malformed_Span => "<malformed>"
+ }
+ }
+ case class Command_Span(name: String, pos: Position.T) extends Kind
+ case object Ignored_Span extends Kind
+ case object Malformed_Span extends Kind
+
+ sealed case class Span(kind: Kind, content: List[Token])
+ {
+ def compact_source: (String, Span) =
+ {
+ val source: String =
+ content match {
+ case List(tok) => tok.source
+ case toks => toks.map(_.source).mkString
+ }
+
+ val content1 = new mutable.ListBuffer[Token]
+ var i = 0
+ for (Token(kind, s) <- content) {
+ val n = s.length
+ val s1 = source.substring(i, i + n)
+ content1 += Token(kind, s1)
+ i += n
+ }
+ (source, Span(kind, content1.toList))
+ }
+ }
+
+ val empty: Span = Span(Ignored_Span, Nil)
+
+ def unparsed(source: String): Span =
+ Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
+
+
+ /* resolve inlined files */
+
+ private def find_file(tokens: List[Token]): Option[String] =
+ {
+ def clean(toks: List[Token]): List[Token] =
+ toks match {
+ case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
+ case t :: ts => t :: clean(ts)
+ case Nil => Nil
+ }
+ clean(tokens.filter(_.is_proper)) match {
+ case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
+ case _ => None
+ }
+ }
+
+ def span_files(syntax: Prover.Syntax, span: Span): List[String] =
+ span.kind match {
+ case Command_Span(name, _) =>
+ syntax.load_command(name) match {
+ case Some(exts) =>
+ find_file(span.content) match {
+ case Some(file) =>
+ if (exts.isEmpty) List(file)
+ else exts.map(ext => file + "." + ext)
+ case None => Nil
+ }
+ case None => Nil
+ }
+ case _ => Nil
+ }
+
+ def resolve_files(
+ resources: Resources,
+ syntax: Prover.Syntax,
+ node_name: Document.Node.Name,
+ span: Span,
+ get_blob: Document.Node.Name => Option[Document.Blob])
+ : List[Command.Blob] =
+ {
+ span_files(syntax, span).map(file_name =>
+ Exn.capture {
+ val name =
+ Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
+ val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
+ (name, blob)
+ })
+ }
+}
+
--- a/src/Pure/PIDE/document.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/PIDE/document.ML Tue Aug 12 20:42:39 2014 +0200
@@ -318,7 +318,7 @@
val span =
Lazy.lazy (fn () =>
Position.setmp_thread_data (Position.id_only id)
- (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
+ (fn () => Outer_Syntax.scan (Keyword.get_lexicons ()) (Position.id id) text) ());
val _ =
Position.setmp_thread_data (Position.id_only id)
(fn () => Output.status (Markup.markup_only Markup.accepted)) ();
--- a/src/Pure/PIDE/markup_tree.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Tue Aug 12 20:42:39 2014 +0200
@@ -261,7 +261,7 @@
make_body(root_range, Nil, overlapping(root_range))
}
- override def toString =
+ override def toString: String =
branches.toList.map(_._2) match {
case Nil => "Empty"
case list => list.mkString("Tree(", ",", ")")
--- a/src/Pure/PIDE/protocol.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue Aug 12 20:42:39 2014 +0200
@@ -312,17 +312,21 @@
def message_positions(
self_id: Document_ID.Generic => Boolean,
+ command_position: Position.T,
chunk_name: Symbol.Text_Chunk.Name,
chunk: Symbol.Text_Chunk,
message: XML.Elem): Set[Text.Range] =
{
def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
props match {
- case Position.Reported(id, name, symbol_range)
- if self_id(id) && name == chunk_name =>
- chunk.incorporate(symbol_range) match {
- case Some(range) => set + range
- case _ => set
+ case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
+ Position.Range.unapply(props) orElse Position.Range.unapply(command_position) match {
+ case Some(symbol_range) =>
+ chunk.incorporate(symbol_range) match {
+ case Some(range) => set + range
+ case _ => set
+ }
+ case None => set
}
case _ => set
}
@@ -343,8 +347,25 @@
}
-trait Protocol extends Prover
+trait Protocol
{
+ /* text */
+
+ def encode(s: String): String
+ def decode(s: String): String
+
+ object Encode
+ {
+ val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
+ }
+
+
+ /* protocol commands */
+
+ def protocol_command_bytes(name: String, args: Bytes*): Unit
+ def protocol_command(name: String, args: String*): Unit
+
+
/* options */
def options(opts: Options): Unit =
--- a/src/Pure/PIDE/prover.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/PIDE/prover.scala Tue Aug 12 20:42:39 2014 +0200
@@ -1,12 +1,15 @@
/* Title: Pure/PIDE/prover.scala
Author: Makarius
-General prover operations.
+General prover operations and process wrapping.
*/
package isabelle
+import java.io.{InputStream, OutputStream, BufferedReader, BufferedOutputStream, IOException}
+
+
object Prover
{
/* syntax */
@@ -14,12 +17,23 @@
trait Syntax
{
def add_keywords(keywords: Thy_Header.Keywords): Syntax
- def scan(input: CharSequence): List[Token]
- def load(span: List[Token]): Option[List[String]]
+ def parse_spans(input: CharSequence): List[Command_Span.Span]
+ def load_command(name: String): Option[List[String]]
def load_commands_in(text: String): Boolean
}
+ /* underlying system process */
+
+ trait System_Process
+ {
+ def stdout: BufferedReader
+ def stderr: BufferedReader
+ def terminate: Unit
+ def join: Int
+ }
+
+
/* messages */
sealed abstract class Message
@@ -68,44 +82,287 @@
}
-trait Prover
+abstract class Prover(
+ receiver: Prover.Message => Unit,
+ system_channel: System_Channel,
+ system_process: Prover.System_Process) extends Protocol
{
- /* text and tree data */
+ /* output */
+
+ val xml_cache: XML.Cache = new XML.Cache()
+
+ private def system_output(text: String)
+ {
+ receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
+ }
+
+ private def protocol_output(props: Properties.T, bytes: Bytes)
+ {
+ receiver(new Prover.Protocol_Output(props, bytes))
+ }
+
+ private def output(kind: String, props: Properties.T, body: XML.Body)
+ {
+ if (kind == Markup.INIT) system_channel.accepted()
- def encode(s: String): String
- def decode(s: String): String
+ val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
+ val reports = Protocol.message_reports(props, body)
+ for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
+ }
+
+ private def exit_message(rc: Int)
+ {
+ output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString)))
+ }
+
+
- object Encode
+ /** process manager **/
+
+ private val (_, process_result) =
+ Simple_Thread.future("process_result") { system_process.join }
+
+ private def terminate_process()
{
- val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
+ try { system_process.terminate }
+ catch {
+ case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
+ }
}
- def xml_cache: XML.Cache
+ private val process_manager = Simple_Thread.fork("process_manager")
+ {
+ val (startup_failed, startup_errors) =
+ {
+ var finished: Option[Boolean] = None
+ val result = new StringBuilder(100)
+ while (finished.isEmpty && (system_process.stderr.ready || !process_result.is_finished)) {
+ while (finished.isEmpty && system_process.stderr.ready) {
+ try {
+ val c = system_process.stderr.read
+ if (c == 2) finished = Some(true)
+ else result += c.toChar
+ }
+ catch { case _: IOException => finished = Some(false) }
+ }
+ Thread.sleep(10)
+ }
+ (finished.isEmpty || !finished.get, result.toString.trim)
+ }
+ if (startup_errors != "") system_output(startup_errors)
+
+ if (startup_failed) {
+ terminate_process()
+ process_result.join
+ exit_message(127)
+ }
+ else {
+ val (command_stream, message_stream) = system_channel.rendezvous()
+
+ command_input_init(command_stream)
+ val stdout = physical_output(false)
+ val stderr = physical_output(true)
+ val message = message_output(message_stream)
+
+ val rc = process_result.join
+ system_output("process terminated")
+ command_input_close()
+ for (thread <- List(stdout, stderr, message)) thread.join
+ system_output("process_manager terminated")
+ exit_message(rc)
+ }
+ system_channel.accepted()
+ }
+
+
+ /* management methods */
+
+ def join() { process_manager.join() }
+
+ def terminate()
+ {
+ command_input_close()
+ system_output("Terminating prover process")
+ terminate_process()
+ }
+
+
+
+ /** process streams **/
+
+ /* command input */
+
+ private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
+
+ private def command_input_close(): Unit = command_input.foreach(_.shutdown)
+
+ private def command_input_init(raw_stream: OutputStream)
+ {
+ val name = "command_input"
+ val stream = new BufferedOutputStream(raw_stream)
+ command_input =
+ Some(
+ Consumer_Thread.fork(name)(
+ consume =
+ {
+ case chunks =>
+ try {
+ Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream)
+ chunks.foreach(_.write(stream))
+ stream.flush
+ true
+ }
+ catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
+ },
+ finish = { case () => stream.close; system_output(name + " terminated") }
+ )
+ )
+ }
- /* process management */
+ /* physical output */
+
+ private def physical_output(err: Boolean): Thread =
+ {
+ val (name, reader, markup) =
+ if (err) ("standard_error", system_process.stderr, Markup.STDERR)
+ else ("standard_output", system_process.stdout, Markup.STDOUT)
- def join(): Unit
- def terminate(): Unit
-
- def protocol_command_bytes(name: String, args: Bytes*): Unit
- def protocol_command(name: String, args: String*): Unit
+ Simple_Thread.fork(name) {
+ try {
+ var result = new StringBuilder(100)
+ var finished = false
+ while (!finished) {
+ //{{{
+ var c = -1
+ var done = false
+ while (!done && (result.length == 0 || reader.ready)) {
+ c = reader.read
+ if (c >= 0) result.append(c.asInstanceOf[Char])
+ else done = true
+ }
+ if (result.length > 0) {
+ output(markup, Nil, List(XML.Text(decode(result.toString))))
+ result.length = 0
+ }
+ else {
+ reader.close
+ finished = true
+ }
+ //}}}
+ }
+ }
+ catch { case e: IOException => system_output(name + ": " + e.getMessage) }
+ system_output(name + " terminated")
+ }
+ }
- /* PIDE protocol commands */
+ /* message output */
+
+ private def message_output(stream: InputStream): Thread =
+ {
+ class EOF extends Exception
+ class Protocol_Error(msg: String) extends Exception(msg)
+
+ val name = "message_output"
+ Simple_Thread.fork(name) {
+ val default_buffer = new Array[Byte](65536)
+ var c = -1
- def options(opts: Options): Unit
+ def read_int(): Int =
+ //{{{
+ {
+ var n = 0
+ c = stream.read
+ if (c == -1) throw new EOF
+ while (48 <= c && c <= 57) {
+ n = 10 * n + (c - 48)
+ c = stream.read
+ }
+ if (c != 10)
+ throw new Protocol_Error("malformed header: expected integer followed by newline")
+ else n
+ }
+ //}}}
- def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit
- def define_command(command: Command): Unit
+ def read_chunk_bytes(): (Array[Byte], Int) =
+ //{{{
+ {
+ val n = read_int()
+ val buf =
+ if (n <= default_buffer.size) default_buffer
+ else new Array[Byte](n)
+
+ var i = 0
+ var m = 0
+ do {
+ m = stream.read(buf, i, n - i)
+ if (m != -1) i += m
+ }
+ while (m != -1 && n > i)
+
+ if (i != n)
+ throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
+
+ (buf, n)
+ }
+ //}}}
- def discontinue_execution(): Unit
- def cancel_exec(id: Document_ID.Exec): Unit
+ def read_chunk(): XML.Body =
+ {
+ val (buf, n) = read_chunk_bytes()
+ YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n))
+ }
- def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
- edits: List[Document.Edit_Command]): Unit
- def remove_versions(versions: List[Document.Version]): Unit
+ try {
+ do {
+ try {
+ val header = read_chunk()
+ header match {
+ case List(XML.Elem(Markup(name, props), Nil)) =>
+ val kind = name.intern
+ if (kind == Markup.PROTOCOL) {
+ val (buf, n) = read_chunk_bytes()
+ protocol_output(props, Bytes(buf, 0, n))
+ }
+ else {
+ val body = read_chunk()
+ output(kind, props, body)
+ }
+ case _ =>
+ read_chunk()
+ throw new Protocol_Error("bad header: " + header.toString)
+ }
+ }
+ catch { case _: EOF => }
+ }
+ while (c != -1)
+ }
+ catch {
+ case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
+ case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
+ }
+ stream.close
- def dialog_result(serial: Long, result: String): Unit
+ system_output(name + " terminated")
+ }
+ }
+
+
+
+ /** protocol commands **/
+
+ def protocol_command_bytes(name: String, args: Bytes*): Unit =
+ command_input match {
+ case Some(thread) => thread.send(Bytes(name) :: args.toList)
+ case None => error("Uninitialized command input thread")
+ }
+
+ def protocol_command(name: String, args: String*)
+ {
+ receiver(new Prover.Input(name, args.toList))
+ protocol_command_bytes(name, args.map(Bytes(_)): _*)
+ }
}
--- a/src/Pure/PIDE/resources.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/PIDE/resources.ML Tue Aug 12 20:42:39 2014 +0200
@@ -132,7 +132,7 @@
fun excursion master_dir last_timing init elements =
let
fun prepare_span span =
- Thy_Syntax.span_content span
+ Command_Span.content span
|> Command.read init master_dir []
|> (fn tr => Toplevel.put_timing (last_timing tr) tr);
@@ -157,8 +157,8 @@
val _ = Thy_Header.define_keywords header;
val lexs = Keyword.get_lexicons ();
- val toks = Thy_Syntax.parse_tokens lexs text_pos text;
- val spans = Thy_Syntax.parse_spans toks;
+ val toks = Outer_Syntax.scan lexs text_pos text;
+ val spans = Outer_Syntax.parse_spans toks;
val elements = Thy_Syntax.parse_elements spans;
fun init () =
--- a/src/Pure/PIDE/resources.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/PIDE/resources.scala Tue Aug 12 20:42:39 2014 +0200
@@ -56,8 +56,8 @@
def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
if (syntax.load_commands_in(text)) {
- val spans = Thy_Syntax.parse_spans(syntax.scan(text))
- spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
+ val spans = syntax.parse_spans(text)
+ spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
}
else Nil
@@ -126,6 +126,6 @@
/* prover process */
def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
- new Isabelle_Process(receiver, args) with Protocol
+ Isabelle_Process(receiver, args)
}
--- a/src/Pure/PIDE/text.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/PIDE/text.scala Tue Aug 12 20:42:39 2014 +0200
@@ -40,7 +40,7 @@
if (start > stop)
error("Bad range: [" + start.toString + ":" + stop.toString + "]")
- override def toString = "[" + start.toString + ":" + stop.toString + "]"
+ override def toString: String = "[" + start.toString + ":" + stop.toString + "]"
def length: Int = stop - start
@@ -116,7 +116,7 @@
case other: Perspective => ranges == other.ranges
case _ => false
}
- override def toString = ranges.toString
+ override def toString: String = ranges.toString
}
@@ -141,7 +141,7 @@
final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
{
- override def toString =
+ override def toString: String =
(if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
--- a/src/Pure/PIDE/xml.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/PIDE/xml.scala Tue Aug 12 20:42:39 2014 +0200
@@ -21,7 +21,7 @@
type Attributes = Properties.T
- sealed abstract class Tree { override def toString = string_of_tree(this) }
+ sealed abstract class Tree { override def toString: String = string_of_tree(this) }
case class Elem(markup: Markup, body: List[Tree]) extends Tree
{
def name: String = markup.name
@@ -150,12 +150,17 @@
private def trim_bytes(s: String): String = new String(s.toCharArray)
private def cache_string(x: String): String =
- lookup(x) match {
- case Some(y) => y
- case None =>
- val z = trim_bytes(x)
- if (z.length > max_string) z else store(z)
- }
+ if (x == "true") "true"
+ else if (x == "false") "false"
+ else if (x == "0.0") "0.0"
+ else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
+ else
+ lookup(x) match {
+ case Some(y) => y
+ case None =>
+ val z = trim_bytes(x)
+ if (z.length > max_string) z else store(z)
+ }
private def cache_props(x: Properties.T): Properties.T =
if (x.isEmpty) x
else
@@ -214,9 +219,9 @@
/* atomic values */
- def long_atom(i: Long): String = i.toString
+ def long_atom(i: Long): String = Library.signed_string_of_long(i)
- def int_atom(i: Int): String = i.toString
+ def int_atom(i: Int): String = Library.signed_string_of_int(i)
def bool_atom(b: Boolean): String = if (b) "1" else "0"
--- a/src/Pure/ROOT Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/ROOT Tue Aug 12 20:42:39 2014 +0200
@@ -160,6 +160,7 @@
"ML/ml_syntax.ML"
"PIDE/active.ML"
"PIDE/command.ML"
+ "PIDE/command_span.ML"
"PIDE/document.ML"
"PIDE/document_id.ML"
"PIDE/execution.ML"
--- a/src/Pure/ROOT.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/ROOT.ML Tue Aug 12 20:42:39 2014 +0200
@@ -236,6 +236,7 @@
(*theory sources*)
use "Thy/thy_header.ML";
+use "PIDE/command_span.ML";
use "Thy/thy_syntax.ML";
use "Thy/html.ML";
use "Thy/latex.ML";
--- a/src/Pure/System/isabelle_font.scala Tue Aug 12 17:18:12 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-/* Title: Pure/System/isabelle_font.scala
- Author: Makarius
-
-Isabelle font support.
-*/
-
-package isabelle
-
-
-import java.awt.{GraphicsEnvironment, Font}
-import java.io.{FileInputStream, BufferedInputStream}
-import javafx.scene.text.{Font => JFX_Font}
-
-
-object Isabelle_Font
-{
- def apply(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
- new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
-
- def install_fonts()
- {
- val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
- for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
- ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
- }
-
- def install_fonts_jfx()
- {
- for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS"))) {
- val stream = new BufferedInputStream(new FileInputStream(font.file))
- try { JFX_Font.loadFont(stream, 1.0) }
- finally { stream.close }
- }
- }
-}
-
--- a/src/Pure/System/isabelle_process.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/System/isabelle_process.ML Tue Aug 12 20:42:39 2014 +0200
@@ -1,8 +1,7 @@
(* Title: Pure/System/isabelle_process.ML
Author: Makarius
-Isabelle process wrapper, based on private fifos for maximum
-robustness and performance, or local socket for maximum portability.
+Isabelle process wrapper.
*)
signature ISABELLE_PROCESS =
@@ -108,8 +107,12 @@
fun standard_message props name body =
if forall (fn s => s = "") body then ()
else
- message name
- (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
+ let
+ val props' =
+ (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
+ (false, SOME id') => props @ [(Markup.idN, id')]
+ | _ => props);
+ in message name props' body end;
in
Output.status_fn := standard_message [] Markup.statusN;
Output.report_fn := standard_message [] Markup.reportN;
--- a/src/Pure/System/isabelle_process.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/System/isabelle_process.scala Tue Aug 12 20:42:39 2014 +0200
@@ -1,318 +1,43 @@
/* Title: Pure/System/isabelle_process.scala
Author: Makarius
- Options: :folding=explicit:collapseFolds=1:
-Isabelle process management -- always reactive due to multi-threaded I/O.
+Isabelle process wrapper.
*/
package isabelle
-import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException}
-
-
-class Isabelle_Process(
- receiver: Prover.Message => Unit = Console.println(_),
- prover_args: List[String] = Nil)
+object Isabelle_Process
{
- /* text and tree data */
-
- def encode(s: String): String = Symbol.encode(s)
- def decode(s: String): String = Symbol.decode(s)
-
- val xml_cache = new XML.Cache()
-
-
- /* output */
-
- private def system_output(text: String)
- {
- receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
- }
-
- private def protocol_output(props: Properties.T, bytes: Bytes)
- {
- receiver(new Prover.Protocol_Output(props, bytes))
- }
-
- private def output(kind: String, props: Properties.T, body: XML.Body)
- {
- if (kind == Markup.INIT) system_channel.accepted()
-
- val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
- val reports = Protocol.message_reports(props, body)
- for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
- }
-
- private def exit_message(rc: Int)
- {
- output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString)))
- }
-
-
-
- /** process manager **/
-
- def command_line(channel: System_Channel, args: List[String]): List[String] =
- Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: (channel.isabelle_args ::: args)
-
- private val system_channel = System_Channel()
-
- private val process =
- try {
- val cmdline = command_line(system_channel, prover_args)
- new Isabelle_System.Managed_Process(null, null, false, cmdline: _*)
- }
- catch { case e: IOException => system_channel.accepted(); throw(e) }
-
- private val (_, process_result) =
- Simple_Thread.future("process_result") { process.join }
-
- private def terminate_process()
+ def apply(
+ receiver: Prover.Message => Unit = Console.println(_),
+ prover_args: List[String] = Nil): Isabelle_Process =
{
- try { process.terminate }
- catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) }
- }
-
- private val process_manager = Simple_Thread.fork("process_manager")
- {
- val (startup_failed, startup_errors) =
- {
- var finished: Option[Boolean] = None
- val result = new StringBuilder(100)
- while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
- while (finished.isEmpty && process.stderr.ready) {
- try {
- val c = process.stderr.read
- if (c == 2) finished = Some(true)
- else result += c.toChar
- }
- catch { case _: IOException => finished = Some(false) }
- }
- Thread.sleep(10)
+ val system_channel = System_Channel()
+ val system_process =
+ try {
+ val cmdline =
+ Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
+ (system_channel.prover_args ::: prover_args)
+ val process =
+ new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
+ Prover.System_Process
+ process.stdin.close
+ process
}
- (finished.isEmpty || !finished.get, result.toString.trim)
- }
- if (startup_errors != "") system_output(startup_errors)
+ catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) }
- process.stdin.close
- if (startup_failed) {
- terminate_process()
- process_result.join
- exit_message(127)
- }
- else {
- val (command_stream, message_stream) = system_channel.rendezvous()
-
- command_input_init(command_stream)
- val stdout = physical_output(false)
- val stderr = physical_output(true)
- val message = message_output(message_stream)
+ new Isabelle_Process(receiver, system_channel, system_process)
+ }
+}
- val rc = process_result.join
- system_output("process terminated")
- command_input_close()
- for (thread <- List(stdout, stderr, message)) thread.join
- system_output("process_manager terminated")
- exit_message(rc)
- }
- system_channel.accepted()
- }
-
-
- /* management methods */
-
- def join() { process_manager.join() }
-
- def interrupt()
+class Isabelle_Process private(
+ receiver: Prover.Message => Unit,
+ system_channel: System_Channel,
+ system_process: Prover.System_Process)
+ extends Prover(receiver, system_channel, system_process)
{
- try { process.interrupt }
- catch { case e: IOException => system_output("Failed to interrupt Isabelle: " + e.getMessage) }
- }
-
- def terminate()
- {
- command_input_close()
- system_output("Terminating Isabelle process")
- terminate_process()
+ def encode(s: String): String = Symbol.encode(s)
+ def decode(s: String): String = Symbol.decode(s)
}
-
-
- /** process streams **/
-
- /* command input */
-
- private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
-
- private def command_input_close(): Unit = command_input.foreach(_.shutdown)
-
- private def command_input_init(raw_stream: OutputStream)
- {
- val name = "command_input"
- val stream = new BufferedOutputStream(raw_stream)
- command_input =
- Some(
- Consumer_Thread.fork(name)(
- consume =
- {
- case chunks =>
- try {
- Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream)
- chunks.foreach(_.write(stream))
- stream.flush
- true
- }
- catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
- },
- finish = { case () => stream.close; system_output(name + " terminated") }
- )
- )
- }
-
-
- /* physical output */
-
- private def physical_output(err: Boolean): Thread =
- {
- val (name, reader, markup) =
- if (err) ("standard_error", process.stderr, Markup.STDERR)
- else ("standard_output", process.stdout, Markup.STDOUT)
-
- Simple_Thread.fork(name) {
- try {
- var result = new StringBuilder(100)
- var finished = false
- while (!finished) {
- //{{{
- var c = -1
- var done = false
- while (!done && (result.length == 0 || reader.ready)) {
- c = reader.read
- if (c >= 0) result.append(c.asInstanceOf[Char])
- else done = true
- }
- if (result.length > 0) {
- output(markup, Nil, List(XML.Text(decode(result.toString))))
- result.length = 0
- }
- else {
- reader.close
- finished = true
- }
- //}}}
- }
- }
- catch { case e: IOException => system_output(name + ": " + e.getMessage) }
- system_output(name + " terminated")
- }
- }
-
-
- /* message output */
-
- private def message_output(stream: InputStream): Thread =
- {
- class EOF extends Exception
- class Protocol_Error(msg: String) extends Exception(msg)
-
- val name = "message_output"
- Simple_Thread.fork(name) {
- val default_buffer = new Array[Byte](65536)
- var c = -1
-
- def read_int(): Int =
- //{{{
- {
- var n = 0
- c = stream.read
- if (c == -1) throw new EOF
- while (48 <= c && c <= 57) {
- n = 10 * n + (c - 48)
- c = stream.read
- }
- if (c != 10)
- throw new Protocol_Error("malformed header: expected integer followed by newline")
- else n
- }
- //}}}
-
- def read_chunk_bytes(): (Array[Byte], Int) =
- //{{{
- {
- val n = read_int()
- val buf =
- if (n <= default_buffer.size) default_buffer
- else new Array[Byte](n)
-
- var i = 0
- var m = 0
- do {
- m = stream.read(buf, i, n - i)
- if (m != -1) i += m
- }
- while (m != -1 && n > i)
-
- if (i != n)
- throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
-
- (buf, n)
- }
- //}}}
-
- def read_chunk(): XML.Body =
- {
- val (buf, n) = read_chunk_bytes()
- YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n))
- }
-
- try {
- do {
- try {
- val header = read_chunk()
- header match {
- case List(XML.Elem(Markup(name, props), Nil)) =>
- val kind = name.intern
- if (kind == Markup.PROTOCOL) {
- val (buf, n) = read_chunk_bytes()
- protocol_output(props, Bytes(buf, 0, n))
- }
- else {
- val body = read_chunk()
- output(kind, props, body)
- }
- case _ =>
- read_chunk()
- throw new Protocol_Error("bad header: " + header.toString)
- }
- }
- catch { case _: EOF => }
- }
- while (c != -1)
- }
- catch {
- case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
- case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
- }
- stream.close
-
- system_output(name + " terminated")
- }
- }
-
-
-
- /** protocol commands **/
-
- def protocol_command_bytes(name: String, args: Bytes*): Unit =
- command_input match {
- case Some(thread) => thread.send(Bytes(name) :: args.toList)
- case None => error("Uninitialized command input thread")
- }
-
- def protocol_command(name: String, args: String*)
- {
- receiver(new Prover.Input(name, args.toList))
- protocol_command_bytes(name, args.map(Bytes(_)): _*)
- }
-}
--- a/src/Pure/System/system_channel.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/System/system_channel.scala Tue Aug 12 20:42:39 2014 +0200
@@ -22,7 +22,7 @@
abstract class System_Channel
{
def params: List[String]
- def isabelle_args: List[String]
+ def prover_args: List[String]
def rendezvous(): (OutputStream, InputStream)
def accepted(): Unit
}
@@ -60,7 +60,7 @@
def params: List[String] = List(fifo1, fifo2)
- val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
+ val prover_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
def rendezvous(): (OutputStream, InputStream) =
{
@@ -81,7 +81,7 @@
def params: List[String] = List("127.0.0.1", server.getLocalPort.toString)
- def isabelle_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
+ def prover_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
def rendezvous(): (OutputStream, InputStream) =
{
--- a/src/Pure/Thy/thy_info.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Aug 12 20:42:39 2014 +0200
@@ -380,7 +380,7 @@
fun script_thy pos txt =
let
- val trs = Outer_Syntax.parse pos txt;
+ val trs = Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt;
val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
in Toplevel.end_theory end_pos end_state end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_structure.scala Tue Aug 12 20:42:39 2014 +0200
@@ -0,0 +1,71 @@
+/* Title: Pure/Thy/thy_structure.scala
+ Author: Makarius
+
+Nested structure of theory source.
+*/
+
+package isabelle
+
+
+import scala.collection.mutable
+import scala.annotation.tailrec
+
+
+object Thy_Structure
+{
+ sealed abstract class Entry { def length: Int }
+ case class Block(val name: String, val body: List[Entry]) extends Entry
+ {
+ val length: Int = (0 /: body)(_ + _.length)
+ }
+ case class Atom(val command: Command) extends Entry
+ {
+ def length: Int = command.length
+ }
+
+ def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
+ {
+ /* stack operations */
+
+ def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
+ var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
+ List((0, node_name.toString, buffer()))
+
+ @tailrec def close(level: Int => Boolean)
+ {
+ stack match {
+ case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
+ body2 += Block(name, body.toList)
+ stack = stack.tail
+ close(level)
+ case _ =>
+ }
+ }
+
+ def result(): Entry =
+ {
+ close(_ => true)
+ val (_, name, body) = stack.head
+ Block(name, body.toList)
+ }
+
+ def add(command: Command)
+ {
+ syntax.heading_level(command) match {
+ case Some(i) =>
+ close(_ > i)
+ stack = (i + 1, command.source, buffer()) :: stack
+ case None =>
+ }
+ stack.head._3 += Atom(command)
+ }
+
+
+ /* result structure */
+
+ val spans = syntax.parse_spans(text)
+ spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
+ result()
+ }
+}
+
--- a/src/Pure/Thy/thy_syntax.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Tue Aug 12 20:42:39 2014 +0200
@@ -6,39 +6,21 @@
signature THY_SYNTAX =
sig
- val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
val reports_of_tokens: Token.T list -> bool * Position.report_text list
val present_token: Token.T -> Output.output
- datatype span_kind = Command of string * Position.T | Ignored | Malformed
- datatype span = Span of span_kind * Token.T list
- val span_kind: span -> span_kind
- val span_content: span -> Token.T list
- val present_span: span -> Output.output
- val parse_spans: Token.T list -> span list
- val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
+ val present_span: Command_Span.span -> Output.output
datatype 'a element = Element of 'a * ('a element list * 'a) option
val atom: 'a -> 'a element
val map_element: ('a -> 'b) -> 'a element -> 'b element
val flat_element: 'a element -> 'a list
val last_element: 'a element -> 'a
- val parse_elements: span list -> span element list
+ val parse_elements: Command_Span.span list -> Command_Span.span element list
end;
structure Thy_Syntax: THY_SYNTAX =
struct
-(** tokens **)
-
-(* parse *)
-
-fun parse_tokens lexs pos =
- Source.of_string #>
- Symbol.source #>
- Token.source {do_recover = SOME false} (K lexs) pos #>
- Source.exhaust;
-
-
-(* present *)
+(** presentation **)
local
@@ -60,97 +42,12 @@
let val results = map reports_of_token toks
in (exists fst results, maps snd results) end;
+end;
+
fun present_token tok =
Markup.enclose (Token.markup tok) (Output.output (Token.unparse tok));
-end;
-
-
-
-(** spans **)
-
-(* type span *)
-
-datatype span_kind = Command of string * Position.T | Ignored | Malformed;
-datatype span = Span of span_kind * Token.T list;
-
-fun span_kind (Span (k, _)) = k;
-fun span_content (Span (_, toks)) = toks;
-
-val present_span = implode o map present_token o span_content;
-
-
-(* parse *)
-
-local
-
-fun make_span toks =
- if not (null toks) andalso Token.is_command (hd toks) then
- Span (Command (Token.content_of (hd toks), Token.pos_of (hd toks)), toks)
- else if forall Token.is_improper toks then Span (Ignored, toks)
- else Span (Malformed, toks);
-
-fun flush (result, span, improper) =
- result
- |> not (null span) ? cons (rev span)
- |> not (null improper) ? cons (rev improper);
-
-fun parse tok (result, span, improper) =
- if Token.is_command tok then (flush (result, span, improper), [tok], [])
- else if Token.is_improper tok then (result, span, tok :: improper)
- else (result, tok :: (improper @ span), []);
-
-in
-
-fun parse_spans toks =
- fold parse toks ([], [], [])
- |> flush |> rev |> map make_span;
-
-end;
-
-
-(* inlined files *)
-
-local
-
-fun clean ((i1, t1) :: (i2, t2) :: toks) =
- if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
- else (i1, t1) :: clean ((i2, t2) :: toks)
- | clean toks = toks;
-
-fun clean_tokens toks =
- ((0 upto length toks - 1) ~~ toks)
- |> filter (fn (_, tok) => Token.is_proper tok)
- |> clean;
-
-fun find_file ((_, tok) :: toks) =
- if Token.is_command tok then
- toks |> get_first (fn (i, tok) =>
- if Token.is_name tok then
- SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
- handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
- else NONE)
- else NONE
- | find_file [] = NONE;
-
-in
-
-fun resolve_files read_files span =
- (case span of
- Span (Command (cmd, pos), toks) =>
- if Keyword.is_theory_load cmd then
- (case find_file (clean_tokens toks) of
- NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
- | SOME (i, path) =>
- let
- val toks' = toks |> map_index (fn (j, tok) =>
- if i = j then Token.put_files (read_files cmd path) tok
- else tok);
- in Span (Command (cmd, pos), toks') end)
- else span
- | _ => span);
-
-end;
+val present_span = implode o map present_token o Command_Span.content;
@@ -174,9 +71,9 @@
(* scanning spans *)
-val eof = Span (Command ("", Position.none), []);
+val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
-fun is_eof (Span (Command ("", _), _)) = true
+fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
| is_eof _ = false;
val not_eof = not o is_eof;
@@ -189,10 +86,13 @@
local
fun command_with pred =
- Scan.one (fn (Span (Command (name, _), _)) => pred name | _ => false);
+ Scan.one
+ (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
val proof_atom =
- Scan.one (fn (Span (Command (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
+ Scan.one
+ (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => Keyword.is_proof_body name
+ | _ => true) >> atom;
fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;
--- a/src/Pure/Thy/thy_syntax.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Tue Aug 12 20:42:39 2014 +0200
@@ -13,93 +13,6 @@
object Thy_Syntax
{
- /** nested structure **/
-
- object Structure
- {
- sealed abstract class Entry { def length: Int }
- case class Block(val name: String, val body: List[Entry]) extends Entry
- {
- val length: Int = (0 /: body)(_ + _.length)
- }
- case class Atom(val command: Command) extends Entry
- {
- def length: Int = command.length
- }
-
- def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
- {
- /* stack operations */
-
- def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
- var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
- List((0, node_name.toString, buffer()))
-
- @tailrec def close(level: Int => Boolean)
- {
- stack match {
- case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
- body2 += Block(name, body.toList)
- stack = stack.tail
- close(level)
- case _ =>
- }
- }
-
- def result(): Entry =
- {
- close(_ => true)
- val (_, name, body) = stack.head
- Block(name, body.toList)
- }
-
- def add(command: Command)
- {
- syntax.heading_level(command) match {
- case Some(i) =>
- close(_ > i)
- stack = (i + 1, command.source, buffer()) :: stack
- case None =>
- }
- stack.head._3 += Atom(command)
- }
-
-
- /* result structure */
-
- val spans = parse_spans(syntax.scan(text))
- spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
- result()
- }
- }
-
-
-
- /** parse spans **/
-
- def parse_spans(toks: List[Token]): List[List[Token]] =
- {
- val result = new mutable.ListBuffer[List[Token]]
- val span = new mutable.ListBuffer[Token]
- val improper = new mutable.ListBuffer[Token]
-
- def flush()
- {
- if (!span.isEmpty) { result += span.toList; span.clear }
- if (!improper.isEmpty) { result += improper.toList; improper.clear }
- }
- for (tok <- toks) {
- if (tok.is_command) { flush(); span += tok }
- else if (tok.is_improper) improper += tok
- else { span ++= improper; improper.clear; span += tok }
- }
- flush()
-
- result.toList
- }
-
-
-
/** perspective **/
def command_perspective(
@@ -231,58 +144,12 @@
}
- /* inlined files */
-
- private def find_file(tokens: List[Token]): Option[String] =
- {
- def clean(toks: List[Token]): List[Token] =
- toks match {
- case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
- case t :: ts => t :: clean(ts)
- case Nil => Nil
- }
- clean(tokens.filter(_.is_proper)) match {
- case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
- case _ => None
- }
- }
-
- def span_files(syntax: Prover.Syntax, span: List[Token]): List[String] =
- syntax.load(span) match {
- case Some(exts) =>
- find_file(span) match {
- case Some(file) =>
- if (exts.isEmpty) List(file)
- else exts.map(ext => file + "." + ext)
- case None => Nil
- }
- case None => Nil
- }
-
- def resolve_files(
- resources: Resources,
- syntax: Prover.Syntax,
- node_name: Document.Node.Name,
- span: List[Token],
- get_blob: Document.Node.Name => Option[Document.Blob])
- : List[Command.Blob] =
- {
- span_files(syntax, span).map(file_name =>
- Exn.capture {
- val name =
- Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
- val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
- (name, blob)
- })
- }
-
-
/* reparse range of command spans */
@tailrec private def chop_common(
cmds: List[Command],
- blobs_spans: List[(List[Command.Blob], List[Token])])
- : (List[Command], List[(List[Command.Blob], List[Token])]) =
+ blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
+ : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
{
(cmds, blobs_spans) match {
case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
@@ -301,8 +168,8 @@
{
val cmds0 = commands.iterator(first, last).toList
val blobs_spans0 =
- parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
- map(span => (resolve_files(resources, syntax, name, span, get_blob), span))
+ syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
+ map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
@@ -337,8 +204,8 @@
val visible = perspective.commands.toSet
def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
- cmds.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
- .find(_.is_command) getOrElse cmds.last
+ cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || visible(cmd))
+ .find(_.is_proper) getOrElse cmds.last
@tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
cmds.find(_.is_unparsed) match {
--- a/src/Pure/Tools/find_consts.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/Tools/find_consts.ML Tue Aug 12 20:42:39 2014 +0200
@@ -143,7 +143,7 @@
in
fun read_query pos str =
- Outer_Syntax.scan pos str
+ Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
|> filter Token.is_proper
|> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
|> #1;
--- a/src/Pure/Tools/find_theorems.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML Tue Aug 12 20:42:39 2014 +0200
@@ -528,7 +528,7 @@
in
fun read_query pos str =
- Outer_Syntax.scan pos str
+ Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
|> filter Token.is_proper
|> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
|> #1;
--- a/src/Pure/build-jars Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/build-jars Tue Aug 12 20:42:39 2014 +0200
@@ -20,7 +20,7 @@
GUI/gui.scala
GUI/gui_thread.scala
GUI/html5_panel.scala
- GUI/jfx_thread.scala
+ GUI/jfx_gui.scala
GUI/popup.scala
GUI/system_dialog.scala
GUI/wrap_panel.scala
@@ -54,6 +54,7 @@
Isar/token.scala
ML/ml_lex.scala
PIDE/command.scala
+ PIDE/command_span.scala
PIDE/document.scala
PIDE/document_id.scala
PIDE/editor.scala
@@ -71,7 +72,6 @@
System/command_line.scala
System/invoke_scala.scala
System/isabelle_charset.scala
- System/isabelle_font.scala
System/isabelle_process.scala
System/isabelle_system.scala
System/options.scala
@@ -83,6 +83,7 @@
Thy/present.scala
Thy/thy_header.scala
Thy/thy_info.scala
+ Thy/thy_structure.scala
Thy/thy_syntax.scala
Tools/build.scala
Tools/build_console.scala
--- a/src/Pure/library.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/library.ML Tue Aug 12 20:42:39 2014 +0200
@@ -642,14 +642,14 @@
local
val zero = ord "0";
- val small = 10000: int;
- val small_table = Vector.tabulate (small, Int.toString);
+ val small_int = 10000: int;
+ val small_int_table = Vector.tabulate (small_int, Int.toString);
in
fun string_of_int i =
if i < 0 then Int.toString i
else if i < 10 then chr (zero + i)
- else if i < small then Vector.sub (small_table, i)
+ else if i < small_int then Vector.sub (small_int_table, i)
else Int.toString i;
end;
--- a/src/Pure/library.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Pure/library.scala Tue Aug 12 20:42:39 2014 +0200
@@ -32,6 +32,33 @@
error(cat_message(msg1, msg2))
+ /* integers */
+
+ private val small_int = 10000
+ private lazy val small_int_table =
+ {
+ val array = new Array[String](small_int)
+ for (i <- 0 until small_int) array(i) = i.toString
+ array
+ }
+
+ def is_small_int(s: String): Boolean =
+ {
+ val len = s.length
+ 1 <= len && len <= 4 &&
+ s.forall(c => '0' <= c && c <= '9') &&
+ (len == 1 || s(0) != '0')
+ }
+
+ def signed_string_of_long(i: Long): String =
+ if (0 <= i && i < small_int) small_int_table(i.toInt)
+ else i.toString
+
+ def signed_string_of_int(i: Int): String =
+ if (0 <= i && i < small_int) small_int_table(i)
+ else i.toString
+
+
/* separated chunks */
def separate[A](s: A, list: List[A]): List[A] =
--- a/src/Tools/Code/code_target.ML Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Tools/Code/code_target.ML Tue Aug 12 20:42:39 2014 +0200
@@ -695,7 +695,7 @@
let
val ctxt = Proof_Context.init_global (Thy_Info.get_theory thyname);
val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
- (filter Token.is_proper o Outer_Syntax.scan Position.none);
+ (filter Token.is_proper o Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none);
in case parse cmd_expr
of SOME f => (writeln "Now generating code..."; f ctxt)
| NONE => error ("Bad directive " ^ quote cmd_expr)
--- a/src/Tools/jEdit/src/documentation_dockable.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Tue Aug 12 20:42:39 2014 +0200
@@ -24,13 +24,13 @@
private case class Documentation(name: String, title: String, path: Path)
{
- override def toString =
+ override def toString: String =
"<html><b>" + HTML.encode(name) + "</b>: " + HTML.encode(title) + "</html>"
}
private case class Text_File(name: String, path: Path)
{
- override def toString = name
+ override def toString: String = name
}
private val root = new DefaultMutableTreeNode
--- a/src/Tools/jEdit/src/isabelle_logic.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Tue Aug 12 20:42:39 2014 +0200
@@ -24,7 +24,7 @@
private class Logic_Entry(val name: String, val description: String)
{
- override def toString = description
+ override def toString: String = description
}
def logic_selector(autosave: Boolean): Option_Component =
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 12 20:42:39 2014 +0200
@@ -21,7 +21,7 @@
object Isabelle_Sidekick
{
def int_to_pos(offset: Text.Offset): Position =
- new Position { def getOffset = offset; override def toString = offset.toString }
+ new Position { def getOffset = offset; override def toString: String = offset.toString }
class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
{
@@ -39,7 +39,7 @@
override def setStart(start: Position) = _start = start
override def getEnd: Position = _end
override def setEnd(end: Position) = _end = end
- override def toString = _name
+ override def toString: String = _name
}
def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
@@ -95,13 +95,11 @@
node_name: Buffer => Option[Document.Node.Name])
extends Isabelle_Sidekick(name)
{
- import Thy_Syntax.Structure
-
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
- def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
+ def make_tree(offset: Text.Offset, entry: Thy_Structure.Entry): List[DefaultMutableTreeNode] =
entry match {
- case Structure.Block(name, body) =>
+ case Thy_Structure.Block(name, body) =>
val node =
new DefaultMutableTreeNode(
new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
@@ -111,8 +109,8 @@
i + e.length
})
List(node)
- case Structure.Atom(command)
- if command.is_command && syntax.heading_level(command).isEmpty =>
+ case Thy_Structure.Atom(command)
+ if command.is_proper && syntax.heading_level(command).isEmpty =>
val node =
new DefaultMutableTreeNode(
new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
@@ -123,7 +121,7 @@
node_name(buffer) match {
case Some(name) =>
val text = JEdit_Lib.buffer_text(buffer)
- val structure = Structure.parse(syntax, name, text)
+ val structure = Thy_Structure.parse(syntax, name, text)
make_tree(0, structure) foreach (node => data.root.add(node))
true
case None => false
@@ -175,7 +173,7 @@
new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
override def getShortString: String = content
override def getLongString: String = info_text
- override def toString = quote(content) + " " + range.toString
+ override def toString: String = quote(content) + " " + range.toString
})
})
}
--- a/src/Tools/jEdit/src/plugin.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 12 20:42:39 2014 +0200
@@ -373,7 +373,7 @@
PIDE.plugin = this
Isabelle_System.init()
- Isabelle_Font.install_fonts()
+ GUI.install_fonts()
PIDE.options.update(Options.init())
PIDE.completion_history.load()
--- a/src/Tools/jEdit/src/rendering.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Tue Aug 12 20:42:39 2014 +0200
@@ -378,6 +378,8 @@
PIDE.editor.hyperlink_source_file(name, line, offset)
case Position.Def_Id_Offset(id, offset) =>
PIDE.editor.hyperlink_command_id(snapshot, id, offset)
+ case Position.Def_Id(id) =>
+ PIDE.editor.hyperlink_command_id(snapshot, id)
case _ => None
}
opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
@@ -390,6 +392,8 @@
PIDE.editor.hyperlink_source_file(name, line, offset)
case Position.Id_Offset(id, offset) =>
PIDE.editor.hyperlink_command_id(snapshot, id, offset)
+ case Position.Id(id) =>
+ PIDE.editor.hyperlink_command_id(snapshot, id)
case _ => None
}
opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
--- a/src/Tools/jEdit/src/symbols_dockable.scala Tue Aug 12 17:18:12 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Tue Aug 12 20:42:39 2014 +0200
@@ -24,8 +24,8 @@
font =
Symbol.fonts.get(symbol) match {
- case None => Isabelle_Font(size = font_size)
- case Some(font_family) => Isabelle_Font(family = font_family, size = font_size)
+ case None => GUI.font(size = font_size)
+ case Some(font_family) => GUI.font(family = font_family, size = font_size)
}
action =
Action(decoded) {