# HG changeset patch # User wenzelm # Date 1407868959 -7200 # Node ID a2a7c1de4752775fd5b6fa62b47d8281973bdd11 # Parent f7f75b33d6c859bc5d0823e9226bb25c414f6592# Parent f5d73caba4e53e95542cb5ab256a78b354de9555 merged diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Doc/antiquote_setup.ML --- 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); diff -r f7f75b33d6c8 -r a2a7c1de4752 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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] diff -r f7f75b33d6c8 -r a2a7c1de4752 src/HOL/Tools/Lifting/lifting_setup.ML --- 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 diff -r f7f75b33d6c8 -r a2a7c1de4752 src/HOL/Tools/try0.ML --- 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 diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/Concurrent/future.scala --- 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 => "" case Some(Exn.Exn(_)) => "" diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/GUI/gui.scala --- 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)) + } } diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/GUI/html5_panel.scala --- 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 diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/GUI/jfx_gui.scala --- /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 } + } + } + +} diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/GUI/jfx_thread.scala --- 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 - } - } -} diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/General/name_space.ML --- 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 diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/General/position.ML --- 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 diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/General/position.scala --- 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 } } diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/General/properties.scala --- 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 } diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/General/time.scala --- 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" } diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/General/timing.scala --- 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 } diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/Isar/isar_syn.ML --- 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)))); diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/Isar/outer_syntax.ML --- 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 *) diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/Isar/outer_syntax.scala --- 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 = diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/command.ML --- 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 diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/command.scala --- 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) diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/command_span.ML --- /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; + diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/command_span.scala --- /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 "" + case Ignored_Span => "" + case Malformed_Span => "" + } + } + 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) + }) + } +} + diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/document.ML --- 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)) (); diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/markup_tree.scala --- 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(", ",", ")") diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/protocol.scala --- 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 = diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/prover.scala --- 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(_)): _*) + } } diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/resources.ML --- 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 () = diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/resources.scala --- 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) } diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/text.scala --- 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 + ")" diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/PIDE/xml.scala --- 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" diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/ROOT --- 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" diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/ROOT.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"; diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/System/isabelle_font.scala --- 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 } - } - } -} - diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/System/isabelle_process.ML --- 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; diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/System/isabelle_process.scala --- 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(_)): _*) - } -} diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/System/system_channel.scala --- 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) = { diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/Thy/thy_info.ML --- 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; diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/Thy/thy_structure.scala --- /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() + } +} + diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/Thy/thy_syntax.ML --- 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; diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/Thy/thy_syntax.scala --- 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 { diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/Tools/find_consts.ML --- 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; diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/Tools/find_theorems.ML --- 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; diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/build-jars --- 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 diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/library.ML --- 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; diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Pure/library.scala --- 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] = diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Tools/Code/code_target.ML --- 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) diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Tools/jEdit/src/documentation_dockable.scala --- 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.encode(name) + ": " + HTML.encode(title) + "" } private case class Text_File(name: String, path: Path) { - override def toString = name + override def toString: String = name } private val root = new DefaultMutableTreeNode diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Tools/jEdit/src/isabelle_logic.scala --- 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 = diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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 }) }) } diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Tools/jEdit/src/plugin.scala --- 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() diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Tools/jEdit/src/rendering.scala --- 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))) diff -r f7f75b33d6c8 -r a2a7c1de4752 src/Tools/jEdit/src/symbols_dockable.scala --- 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) {