--- a/Admin/update-keywords Tue Aug 07 14:29:18 2012 +0200
+++ b/Admin/update-keywords Tue Aug 07 22:32:14 2012 +0200
@@ -11,10 +11,8 @@
cd "$ISABELLE_HOME/etc"
isabelle keywords \
- "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
- "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
- "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
+ "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" \
+ "$LOG/HOL-Statespace.gz" "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
-isabelle keywords -k ZF \
- "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
+isabelle keywords -k ZF "$LOG/ZF.gz"
--- a/etc/isar-keywords-ZF.el Tue Aug 07 14:29:18 2012 +0200
+++ b/etc/isar-keywords-ZF.el Tue Aug 07 22:32:14 2012 +0200
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + FOL + ZF.
+;; Generated from ZF.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
--- a/etc/isar-keywords.el Tue Aug 07 14:29:18 2012 +0200
+++ b/etc/isar-keywords.el Tue Aug 07 22:32:14 2012 +0200
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
+;; Generated from HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
--- a/src/Pure/General/pretty.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/General/pretty.ML Tue Aug 07 22:32:14 2012 +0200
@@ -21,6 +21,7 @@
signature PRETTY =
sig
+ val spaces: int -> string
val default_indent: string -> int -> Output.output
val add_mode: string -> (string -> int -> Output.output) -> unit
type T
@@ -69,9 +70,22 @@
structure Pretty: PRETTY =
struct
+(** spaces **)
+
+local
+ val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i Symbol.space);
+in
+ fun spaces k =
+ if k < 64 then Vector.sub (small_spaces, k)
+ else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
+ Vector.sub (small_spaces, k mod 64);
+end;
+
+
+
(** print mode operations **)
-fun default_indent (_: string) = Symbol.spaces;
+fun default_indent (_: string) = spaces;
local
val default = {indent = default_indent};
@@ -89,7 +103,7 @@
fun mode_indent x y = #indent (get_mode ()) x y;
-val output_spaces = Output.output o Symbol.spaces;
+val output_spaces = Output.output o spaces;
val add_indent = Buffer.add o output_spaces;
@@ -167,7 +181,7 @@
fun big_list name prts = block (fbreaks (str name :: prts));
fun indent 0 prt = prt
- | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
+ | indent n prt = blk (0, [str (spaces n), prt]);
fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
| unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
--- a/src/Pure/General/pretty.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/General/pretty.scala Tue Aug 07 22:32:14 2012 +0200
@@ -12,6 +12,21 @@
object Pretty
{
+ /* spaces */
+
+ val spc = ' '
+ val space = " "
+
+ private val static_spaces = space * 4000
+
+ def spaces(k: Int): String =
+ {
+ require(k >= 0)
+ if (k < static_spaces.length) static_spaces.substring(0, k)
+ else space * k
+ }
+
+
/* markup trees with physical blocks and breaks */
def block(body: XML.Body): XML.Tree = Block(2, body)
@@ -33,7 +48,7 @@
{
def apply(w: Int): XML.Tree =
XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
- List(XML.Text(Symbol.spaces(w))))
+ List(XML.Text(spaces(w))))
def unapply(tree: XML.Tree): Option[Int] =
tree match {
@@ -59,7 +74,7 @@
{
def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
- def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
+ def blanks(wd: Int): Text = string(spaces(wd), wd.toDouble)
def content: XML.Body = tx.reverse
}
@@ -69,7 +84,7 @@
def font_metric(metrics: FontMetrics): String => Double =
if (metrics == null) ((s: String) => s.length.toDouble)
else {
- val unit = metrics.charWidth(Symbol.spc).toDouble
+ val unit = metrics.charWidth(spc).toDouble
((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
}
@@ -143,8 +158,8 @@
def fmt(tree: XML.Tree): XML.Body =
tree match {
case Block(_, body) => body.flatMap(fmt)
- case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
- case FBreak => List(XML.Text(Symbol.space))
+ case Break(wd) => List(XML.Text(spaces(wd)))
+ case FBreak => List(XML.Text(space))
case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
case XML.Text(_) => List(tree)
}
--- a/src/Pure/General/symbol.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/General/symbol.ML Tue Aug 07 22:32:14 2012 +0200
@@ -10,7 +10,6 @@
val STX: symbol
val DEL: symbol
val space: symbol
- val spaces: int -> string
val is_char: symbol -> bool
val is_utf8: symbol -> bool
val is_symbolic: symbol -> bool
@@ -92,15 +91,6 @@
val space = chr 32;
-local
- val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i space);
-in
- fun spaces k =
- if k < 64 then Vector.sub (small_spaces, k)
- else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
- Vector.sub (small_spaces, k mod 64);
-end;
-
fun is_char s = size s = 1;
fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
--- a/src/Pure/General/symbol.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/General/symbol.scala Tue Aug 07 22:32:14 2012 +0200
@@ -15,21 +15,6 @@
type Symbol = String
- /* spaces */
-
- val spc = ' '
- val space = " "
-
- private val static_spaces = space * 4000
-
- def spaces(k: Int): String =
- {
- require(k >= 0)
- if (k < static_spaces.length) static_spaces.substring(0, k)
- else space * k
- }
-
-
/* ASCII characters */
def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
@@ -345,7 +330,7 @@
"\\<^isub>", "\\<^isup>")
val blanks =
- recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
+ recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
val sym_chars =
Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
--- a/src/Pure/Isar/keyword.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Isar/keyword.ML Tue Aug 07 22:32:14 2012 +0200
@@ -49,7 +49,6 @@
val command_keyword: string -> T option
val command_tags: string -> string list
val dest: unit -> string list * string list
- val keyword_statusN: string
val status: unit -> unit
val define: string * T option -> unit
val is_diag: string -> bool
@@ -183,43 +182,29 @@
(* status *)
-val keyword_statusN = "keyword_status";
-
-fun status_message m s =
- Position.setmp_thread_data Position.none
- (if print_mode_active keyword_statusN then Output.protocol_message m else writeln) s;
-
-fun keyword_status name =
- status_message (Isabelle_Markup.keyword_decl name)
- ("Outer syntax keyword " ^ quote name);
-
-fun command_status (name, kind) =
- status_message (Isabelle_Markup.command_decl name (kind_of kind))
- ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind);
-
fun status () =
let
val {lexicons = (minor, _), commands} = get_keywords ();
- val _ = List.app keyword_status (sort_strings (Scan.dest_lexicon minor));
- val _ = List.app command_status (sort_wrt #1 (Symtab.dest commands));
+ val _ = sort_strings (Scan.dest_lexicon minor) |> List.app (fn name =>
+ writeln ("Outer syntax keyword " ^ quote name));
+ val _ = sort_wrt #1 (Symtab.dest commands) |> List.app (fn (name, kind) =>
+ writeln ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind));
in () end;
(* define *)
-fun define (name, NONE) =
- (change_keywords (fn ((minor, major), commands) =>
- let
- val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
- in ((minor', major), commands) end);
- keyword_status name)
- | define (name, SOME kind) =
- (change_keywords (fn ((minor, major), commands) =>
- let
- val major' = Scan.extend_lexicon (Symbol.explode name) major;
- val commands' = Symtab.update (name, kind) commands;
- in ((minor, major'), commands') end);
- command_status (name, kind));
+fun define (name, opt_kind) = change_keywords (fn ((minor, major), commands) =>
+ (case opt_kind of
+ NONE =>
+ let
+ val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
+ in ((minor', major), commands) end
+ | SOME kind =>
+ let
+ val major' = Scan.extend_lexicon (Symbol.explode name) major;
+ val commands' = Symtab.update (name, kind) commands;
+ in ((minor, major'), commands') end));
(* command categories *)
--- a/src/Pure/Isar/outer_syntax.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Tue Aug 07 22:32:14 2012 +0200
@@ -34,8 +34,6 @@
result.toString
}
- type Decl = (String, Option[(String, List[String])])
-
val empty: Outer_Syntax = new Outer_Syntax()
def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
}
@@ -61,10 +59,13 @@
def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
- def + (decl: Outer_Syntax.Decl): Outer_Syntax =
- decl match {
- case ((name, Some((kind, _)))) => this + (name, kind)
- case ((name, None)) => this + name
+
+ def add_keywords(header: Document.Node.Header): Outer_Syntax =
+ (this /: header.keywords) {
+ case (syntax, ((name, Some((kind, _))))) =>
+ syntax + (Symbol.decode(name), kind) + (Symbol.encode(name), kind)
+ case (syntax, ((name, None))) =>
+ syntax + Symbol.decode(name) + Symbol.encode(name)
}
def is_command(name: String): Boolean =
--- a/src/Pure/Isar/parse.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Isar/parse.scala Tue Aug 07 22:32:14 2012 +0200
@@ -50,9 +50,11 @@
def atom(s: String, pred: Elem => Boolean): Parser[String] =
token(s, pred) ^^ (_.content)
+ def command(name: String): Parser[String] =
+ atom("command " + quote(name), tok => tok.is_command && tok.source == name)
+
def keyword(name: String): Parser[String] =
- atom(Token.Kind.KEYWORD.toString + " " + quote(name),
- tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
+ atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
def string: Parser[String] = atom("string", _.is_string)
def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
--- a/src/Pure/Isar/token.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Isar/token.scala Tue Aug 07 22:32:14 2012 +0200
@@ -67,7 +67,8 @@
sealed case class Token(val kind: Token.Kind.Value, val source: String)
{
def is_command: Boolean = kind == Token.Kind.COMMAND
- def is_operator: Boolean = kind == Token.Kind.KEYWORD && !Symbol.is_ascii_identifier(source)
+ def is_keyword: Boolean = kind == Token.Kind.KEYWORD
+ def is_operator: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
def is_delimited: Boolean =
kind == Token.Kind.STRING ||
kind == Token.Kind.ALT_STRING ||
@@ -90,8 +91,8 @@
def is_proper: Boolean = !is_space && !is_comment
def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
- def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"
- def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"
+ def is_begin: Boolean = is_keyword && source == "begin"
+ def is_end: Boolean = is_keyword && source == "end"
def content: String =
if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
@@ -101,7 +102,7 @@
else source
def text: (String, String) =
- if (kind == Token.Kind.COMMAND && source == ";") ("terminator", "")
+ if (is_command && source == ";") ("terminator", "")
else (kind.toString, source)
}
--- a/src/Pure/PIDE/command.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/command.scala Tue Aug 07 22:32:14 2012 +0200
@@ -133,7 +133,7 @@
def is_command: Boolean = !is_ignored && !is_malformed
def name: String =
- span.find(_.is_command) match { case Some(tok) => tok.content case _ => "" }
+ span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
override def toString =
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
--- a/src/Pure/PIDE/document.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/document.ML Tue Aug 07 22:32:14 2012 +0200
@@ -15,11 +15,11 @@
val new_id: unit -> id
val parse_id: string -> id
val print_id: id -> string
- type node_header = (string * Thy_Header.header) Exn.result
+ type node_header = string * Thy_Header.header * string list
datatype node_edit =
Clear |
Edits of (command_id option * command_id option) list |
- Header of node_header |
+ Deps of node_header |
Perspective of command_id list
type edit = string * node_edit
type state
@@ -59,7 +59,7 @@
(** document structure **)
-type node_header = (string * Thy_Header.header) Exn.result;
+type node_header = string * Thy_Header.header * string list;
type perspective = (command_id -> bool) * command_id option;
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
@@ -67,7 +67,7 @@
val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
abstype node = Node of
- {header: node_header,
+ {header: node_header, (*master directory, theory header, errors*)
perspective: perspective, (*visible commands, last*)
entries: (exec_id * exec) option Entries.T, (*command entries with excecutions*)
result: exec option} (*result of last execution*)
@@ -83,7 +83,7 @@
fun make_perspective command_ids : perspective =
(Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
-val no_header = Exn.Exn (ERROR "Bad theory header");
+val no_header = ("", Thy_Header.make "" [] [] [], ["Bad theory header"]);
val no_perspective = make_perspective [];
val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
@@ -92,7 +92,10 @@
(* basic components *)
-fun get_header (Node {header, ...}) = header;
+fun get_header (Node {header = (master, header, errors), ...}) =
+ if null errors then (master, header)
+ else error (cat_lines errors);
+
fun set_header header =
map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
@@ -128,7 +131,7 @@
datatype node_edit =
Clear |
Edits of (command_id option * command_id option) list |
- Header of node_header |
+ Deps of node_header |
Perspective of command_id list;
type edit = string * node_edit;
@@ -178,22 +181,21 @@
(case node_edit of
Clear => update_node name clear_node nodes
| Edits edits => update_node name (edit_node edits) nodes
- | Header header =>
+ | Deps (master, header, errors) =>
let
- val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
- val header' =
- ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header)
- handle exn as ERROR _ => Exn.Exn exn;
+ val errors1 =
+ (Thy_Header.define_keywords header; errors)
+ handle ERROR msg => errors @ [msg];
val nodes1 = nodes
|> default_node name
- |> fold default_node imports;
+ |> fold default_node (#imports header);
val nodes2 = nodes1
|> Graph.Keys.fold
(fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
- val (header'', nodes3) =
- (header', Graph.add_deps_acyclic (name, imports) nodes2)
- handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
- in Graph.map_node name (set_header header'') nodes3 end
+ val (nodes3, errors2) =
+ (Graph.add_deps_acyclic (name, #imports header) nodes2, errors1)
+ handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
+ in Graph.map_node name (set_header (master, header, errors2)) nodes3 end
| Perspective perspective => update_node name (set_perspective perspective) nodes);
fun put_node (name, node) (Version nodes) =
@@ -374,7 +376,7 @@
fun init_theory imports node =
let
(* FIXME provide files via Scala layer, not master_dir *)
- val (dir, header) = Exn.release (get_header node);
+ val (dir, header) = get_header node;
val master_dir =
(case Url.explode dir of
Url.File path => path
@@ -393,7 +395,7 @@
fun check_theory full name node =
is_some (Thy_Info.lookup_theory name) orelse
- is_some (Exn.get_res (get_header node)) andalso (not full orelse is_some (get_result node));
+ can get_header node andalso (not full orelse is_some (get_result node));
fun last_common state last_visible node0 node =
let
--- a/src/Pure/PIDE/document.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/document.scala Tue Aug 07 22:32:14 2012 +0200
@@ -35,14 +35,18 @@
type Edit_Text = Edit[Text.Edit, Text.Perspective]
type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
- type Node_Header = Exn.Result[Node.Deps]
-
object Node
{
- sealed case class Deps(
+ sealed case class Header(
imports: List[Name],
- keywords: List[Outer_Syntax.Decl],
- uses: List[(String, Boolean)])
+ keywords: Thy_Header.Keywords,
+ uses: List[(String, Boolean)],
+ errors: List[String] = Nil)
+ {
+ def error(msg: String): Header = copy(errors = errors ::: List(msg))
+ }
+
+ def bad_header(msg: String): Header = Header(Nil, Nil, Nil, List(msg))
object Name
{
@@ -83,7 +87,7 @@
}
case class Clear[A, B]() extends Edit[A, B]
case class Edits[A, B](edits: List[A]) extends Edit[A, B]
- case class Header[A, B](header: Node_Header) extends Edit[A, B]
+ case class Deps[A, B](header: Header) extends Edit[A, B]
case class Perspective[A, B](perspective: B) extends Edit[A, B]
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
@@ -103,14 +107,14 @@
}
final class Node private(
- val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
+ val header: Node.Header = Node.bad_header("Bad theory header"),
val perspective: Command.Perspective = Command.Perspective.empty,
val blobs: Map[String, Blob] = Map.empty,
val commands: Linear_Set[Command] = Linear_Set.empty)
{
def clear: Node = new Node(header = header)
- def update_header(new_header: Node_Header): Node =
+ def update_header(new_header: Node.Header): Node =
new Node(new_header, perspective, blobs, commands)
def update_perspective(new_perspective: Command.Perspective): Node =
@@ -122,12 +126,6 @@
def update_commands(new_commands: Linear_Set[Command]): Node =
new Node(header, perspective, blobs, new_commands)
- def imports: List[Node.Name] =
- header match { case Exn.Res(deps) => deps.imports case _ => Nil }
-
- def keywords: List[Outer_Syntax.Decl] =
- header match { case Exn.Res(deps) => deps.keywords case _ => Nil }
-
/* commands */
@@ -190,7 +188,7 @@
def + (entry: (Node.Name, Node)): Nodes =
{
val (name, node) = entry
- val imports = node.imports
+ val imports = node.header.imports
val graph1 =
(graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
--- a/src/Pure/PIDE/isabelle_markup.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML Tue Aug 07 22:32:14 2012 +0200
@@ -102,10 +102,6 @@
val no_reportN: string val no_report: Markup.T
val badN: string val bad: Markup.T
val functionN: string
- val ready: Properties.T
- val loaded_theory: string -> Properties.T
- val keyword_decl: string -> Properties.T
- val command_decl: string -> string -> Properties.T
val assign_execs: Properties.T
val removed_versions: Properties.T
val invoke_scala: string -> string -> Properties.T
@@ -308,14 +304,6 @@
val functionN = "function"
-val ready = [(functionN, "ready")];
-
-fun loaded_theory name = [(functionN, "loaded_theory"), (Markup.nameN, name)];
-
-fun keyword_decl name = [(functionN, "keyword_decl"), (Markup.nameN, name)];
-fun command_decl name kind =
- [(functionN, "command_decl"), (Markup.nameN, name), (Markup.kindN, kind)];
-
val assign_execs = [(functionN, "assign_execs")];
val removed_versions = [(functionN, "removed_versions")];
--- a/src/Pure/PIDE/isabelle_markup.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Tue Aug 07 22:32:14 2012 +0200
@@ -250,35 +250,6 @@
val FUNCTION = "function"
val Function = new Properties.String(FUNCTION)
- val Ready: Properties.T = List((FUNCTION, "ready"))
-
- object Loaded_Theory
- {
- def unapply(props: Properties.T): Option[String] =
- props match {
- case List((FUNCTION, "loaded_theory"), (Markup.NAME, name)) => Some(name)
- case _ => None
- }
- }
-
- object Keyword_Decl
- {
- def unapply(props: Properties.T): Option[String] =
- props match {
- case List((FUNCTION, "keyword_decl"), (Markup.NAME, name)) => Some(name)
- case _ => None
- }
- }
- object Command_Decl
- {
- def unapply(props: Properties.T): Option[(String, String)] =
- props match {
- case List((FUNCTION, "command_decl"), (Markup.NAME, name), (Markup.KIND, kind)) =>
- Some((name, kind))
- case _ => None
- }
- }
-
val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
--- a/src/Pure/PIDE/protocol.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML Tue Aug 07 22:32:14 2012 +0200
@@ -37,16 +37,15 @@
fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
fn ([], a) =>
let
- val ((((master, name), imports), keywords), uses) =
- pair (pair (pair (pair string string) (list string))
- (list (pair string (option (pair string (list string))))))
- (list (pair string bool)) a;
- val res =
- Exn.capture (fn () =>
- (master, Thy_Header.make name imports keywords
- (map (apfst Path.explode) uses))) ();
- in Document.Header res end,
- fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
+ val (master, (name, (imports, (keywords, (uses, errors))))) =
+ pair string (pair string (pair (list string)
+ (pair (list (pair string (option (pair string (list string)))))
+ (pair (list (pair string bool)) (list string))))) a;
+ val (uses', errors') =
+ (map (apfst Path.explode) uses, errors)
+ handle ERROR msg => ([], errors @ [msg]);
+ val header = Thy_Header.make name imports keywords uses';
+ in Document.Deps (master, header, errors') end,
fn (a, []) => Document.Perspective (map int_atom a)]))
end;
--- a/src/Pure/PIDE/protocol.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue Aug 07 22:32:14 2012 +0200
@@ -195,7 +195,7 @@
def define_command(command: Command): Unit =
input("Document.define_command",
- Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
+ Document.ID(command.id), encode(command.name), encode(command.source))
/* document versions */
@@ -210,30 +210,28 @@
val edits_yxml =
{ import XML.Encode._
def id: T[Command] = (cmd => long(cmd.id))
- def symbol_string: T[String] = (s => string(Symbol.encode(s)))
def encode_edit(name: Document.Node.Name)
: T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
variant(List(
{ case Document.Node.Clear() => (Nil, Nil) },
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
- { case Document.Node.Header(Exn.Res(deps)) =>
+ { case Document.Node.Deps(header) =>
val dir = Isabelle_System.posix_path(name.dir)
- val imports = deps.imports.map(_.node)
+ val imports = header.imports.map(_.node)
// FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
- val uses = deps.uses
+ val uses = header.uses
(Nil,
- pair(pair(pair(pair(symbol_string, symbol_string), list(symbol_string)),
- list(pair(symbol_string, option(pair(symbol_string, list(symbol_string)))))),
- list(pair(symbol_string, bool)))(
- (((dir, name.theory), imports), deps.keywords), uses)) },
- { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) },
+ pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
+ pair(list(pair(Encode.string, option(pair(Encode.string, list(Encode.string))))),
+ pair(list(pair(Encode.string, bool)), list(Encode.string))))))(
+ (dir, (name.theory, (imports, (header.keywords, (uses, header.errors))))))) },
{ case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
- def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
+ def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
{
val (name, edit) = node_edit
pair(string, encode_edit(name))(name.node, edit)
})
- YXML.string_of_body(encode(edits)) }
+ YXML.string_of_body(encode_edits(edits)) }
input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
}
--- a/src/Pure/Proof/extraction.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Aug 07 22:32:14 2012 +0200
@@ -120,7 +120,7 @@
fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
fun corr_name s vs = extr_name s vs ^ "_correctness";
-fun msg d s = Output.urgent_message (Symbol.spaces d ^ s);
+fun msg d s = Output.urgent_message (Pretty.spaces d ^ s);
fun vars_of t = map Var (rev (Term.add_vars t []));
fun frees_of t = map Free (rev (Term.add_frees t []));
--- a/src/Pure/System/build.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/build.scala Tue Aug 07 22:32:14 2012 +0200
@@ -163,19 +163,19 @@
/* parser */
+ private val SESSION = "session"
+ private val IN = "in"
+ private val DESCRIPTION = "description"
+ private val OPTIONS = "options"
+ private val THEORIES = "theories"
+ private val FILES = "files"
+
+ lazy val root_syntax =
+ Outer_Syntax.init() + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
+ (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
+
private object Parser extends Parse.Parser
{
- val SESSION = "session"
- val IN = "in"
- val DESCRIPTION = "description"
- val OPTIONS = "options"
- val THEORIES = "theories"
- val FILES = "files"
-
- val syntax =
- Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
- SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
-
def session_entry(pos: Position.T): Parser[Session_Entry] =
{
val session_name = atom("session name", _.is_name)
@@ -188,7 +188,7 @@
keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
{ case _ ~ (x ~ y) => (x, y) }
- ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
+ ((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
(keyword("!") ^^^ true | success(false)) ~
(keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
(opt(keyword(IN) ~! path ^^ { case _ ~ x => x })) ~
@@ -202,7 +202,7 @@
def parse_entries(root: Path): List[Session_Entry] =
{
- val toks = syntax.scan(File.read(root))
+ val toks = root_syntax.scan(File.read(root))
parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
case Success(result, _) => result
case bad => error(bad.toString)
@@ -315,22 +315,22 @@
}
- /* source dependencies */
+ /* source dependencies and static content */
- sealed case class Node(
+ sealed case class Session_Content(
loaded_theories: Set[String],
syntax: Outer_Syntax,
sources: List[(Path, SHA1.Digest)])
- sealed case class Deps(deps: Map[String, Node])
+ sealed case class Deps(deps: Map[String, Session_Content])
{
def is_empty: Boolean = deps.isEmpty
- def apply(name: String): Node = deps(name)
+ def apply(name: String): Session_Content = deps(name)
def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
}
def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
- Deps((Map.empty[String, Node] /: tree.topological_order)(
+ Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
{ case (deps, (name, info)) =>
val (preloaded, parent_syntax) =
info.parent match {
@@ -358,19 +358,12 @@
map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
-
- val keywords = thy_deps.map({ case (_, Exn.Res(h)) => h.keywords case _ => Nil }).flatten
- val syntax = (parent_syntax /: keywords)(_ + _)
+ val syntax = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
val all_files =
thy_deps.map({ case (n, h) =>
val thy = Path.explode(n.node).expand
- val uses =
- h match {
- case Exn.Res(d) =>
- d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
- case _ => Nil
- }
+ val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
thy :: uses
}).flatten ::: info.files.map(file => info.dir + file)
val sources =
@@ -381,9 +374,17 @@
quote(name) + Position.str_of(info.pos))
}
- deps + (name -> Node(loaded_theories, syntax, sources))
+ deps + (name -> Session_Content(loaded_theories, syntax, sources))
}))
+ def session_content(session: String): Session_Content =
+ {
+ val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
+ dependencies(false, tree)(session)
+ }
+
+ def outer_syntax(session: String): Outer_Syntax = session_content(session).syntax
+
/* jobs */
@@ -398,7 +399,7 @@
browser_info + Path.explode("isabelle.gif"))
File.write(browser_info + Path.explode("index.html"),
File.read(Path.explode("~~/lib/html/library_index_header.template")) +
- File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_Session_Content.template")) +
File.read(Path.explode("~~/lib/html/library_index_footer.template")))
}
@@ -702,15 +703,5 @@
}
}
}
-
-
- /* static outer syntax */
-
- // FIXME Symbol.decode!?
- def outer_syntax(session: String): Outer_Syntax =
- {
- val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
- dependencies(false, tree)(session).syntax
- }
}
--- a/src/Pure/System/isabelle_process.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML Tue Aug 07 22:32:14 2012 +0200
@@ -2,17 +2,15 @@
Author: Makarius
Isabelle process wrapper, based on private fifos for maximum
-robustness and performance.
+robustness and performance, or local socket for maximum portability.
Startup phases:
- . raw Posix process startup with uncontrolled output on stdout/stderr
- . stderr \002: ML running
- .. stdin/stdout/stderr freely available (raw ML loop)
- .. protocol thread initialization
- ... rendezvous on system channel
- ... message INIT(pid): channels ready
- ... message RAW(keywords)
- ... message RAW(ready): main loop ready
+ - raw Posix process startup with uncontrolled output on stdout/stderr
+ - stderr \002: ML running
+ - stdin/stdout/stderr freely available (raw ML loop)
+ - protocol thread initialization
+ - rendezvous on system channel
+ - message INIT: channels ready
*)
signature ISABELLE_PROCESS =
@@ -96,7 +94,7 @@
in
-fun setup_channels channel =
+fun init_channels channel =
let
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
@@ -178,15 +176,10 @@
Unsynchronized.change print_mode
(fn mode =>
(mode @ [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN])
- |> fold (update op =)
- [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
+ |> fold (update op =) [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]);
val channel = rendezvous ();
- val _ = setup_channels channel;
-
- val _ = Keyword.status ();
- val _ = Thy_Info.status ();
- val _ = Output.protocol_message Isabelle_Markup.ready "";
+ val _ = init_channels channel;
in loop channel end));
fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
--- a/src/Pure/System/isabelle_process.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala Tue Aug 07 22:32:14 2012 +0200
@@ -83,6 +83,17 @@
import Isabelle_Process._
+ /* text representation */
+
+ def encode(s: String): String = Symbol.encode(s)
+ def decode(s: String): String = Symbol.decode(s)
+
+ object Encode
+ {
+ val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
+ }
+
+
/* output */
private def system_output(text: String)
@@ -264,7 +275,7 @@
else done = true
}
if (result.length > 0) {
- output_message(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
+ output_message(markup, Nil, List(XML.Text(decode(result.toString))))
result.length = 0
}
else {
@@ -323,7 +334,7 @@
val default_buffer = new Array[Byte](65536)
var c = -1
- def read_chunk(decode: Boolean): XML.Body =
+ def read_chunk(do_decode: Boolean): XML.Body =
{
//{{{
// chunk size
@@ -350,8 +361,8 @@
if (i != n) throw new Protocol_Error("bad message chunk content")
- if (decode)
- YXML.parse_body_failsafe(Standard_System.decode_chars(Symbol.decode, buf, 0, n))
+ if (do_decode)
+ YXML.parse_body_failsafe(Standard_System.decode_chars(decode, buf, 0, n))
else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString))
//}}}
}
--- a/src/Pure/System/options.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/options.scala Tue Aug 07 22:32:14 2012 +0200
@@ -30,13 +30,15 @@
/* parsing */
+ private val DECLARE = "declare"
+ private val DEFINE = "define"
+
+ lazy val options_syntax =
+ Outer_Syntax.init() + ":" + "=" + "--" +
+ (DECLARE, Keyword.THY_DECL) + (DEFINE, Keyword.PRF_DECL)
+
private object Parser extends Parse.Parser
{
- val DECLARE = "declare"
- val DEFINE = "define"
-
- val syntax = Outer_Syntax.empty + ":" + "=" + "--" + DECLARE + DEFINE
-
val entry: Parser[Options => Options] =
{
val option_name = atom("option name", _.is_xname)
@@ -47,16 +49,17 @@
{ case s ~ n => if (s.isDefined) "-" + n else n } |
atom("option value", tok => tok.is_name || tok.is_float)
- keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
+ command(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
{ case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) } |
- keyword(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
+ command(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
{ case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
}
def parse_entries(file: Path): List[Options => Options] =
{
- parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.implode)) match {
+ val toks = options_syntax.scan(File.read(file))
+ parse_all(rep(entry), Token.reader(toks, file.implode)) match {
case Success(result, _) => result
case bad => error(bad.toString)
}
--- a/src/Pure/System/session.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/session.ML Tue Aug 07 22:32:14 2012 +0200
@@ -71,6 +71,7 @@
fun finish () =
(Thy_Info.finish ();
Present.finish ();
+ Keyword.status ();
Outer_Syntax.check_syntax ();
Future.shutdown ();
Options.reset_default ();
--- a/src/Pure/System/session.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/session.scala Tue Aug 07 22:32:14 2012 +0200
@@ -37,7 +37,7 @@
}
-class Session(thy_load: Thy_Load = new Thy_Load())
+class Session(val thy_load: Thy_Load = new Thy_Load())
{
/* global flags */
@@ -108,7 +108,7 @@
val prev = previous.get_finished
val (doc_edits, version) =
Timing.timeit("Thy_Syntax.text_edits", timing) {
- Thy_Syntax.text_edits(prover_syntax, prev, text_edits)
+ Thy_Syntax.text_edits(base_syntax, prev, text_edits)
}
version_result.fulfill(version)
sender ! Change(doc_edits, prev, version)
@@ -125,11 +125,7 @@
/* global state */
- @volatile private var prover_syntax =
- Outer_Syntax.init() +
- // FIXME avoid hardwired stuff!?
- ("hence", Keyword.PRF_ASM_GOAL, "then have") +
- ("thus", Keyword.PRF_ASM_GOAL, "then show")
+ @volatile private var base_syntax = Outer_Syntax.init()
private val syslog = Volatile(Queue.empty[XML.Elem])
def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
@@ -149,9 +145,12 @@
def recent_syntax(): Outer_Syntax =
{
val version = current_state().recent_finished.version.get_finished
- if (version.is_init) prover_syntax
+ if (version.is_init) base_syntax
else version.syntax
}
+ def get_recent_syntax(): Option[Outer_Syntax] =
+ if (is_ready) Some(recent_syntax)
+ else None
def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
@@ -160,21 +159,19 @@
/* theory files */
- def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
+ def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
{
- val header1: Document.Node_Header =
- header match {
- case Exn.Res(_) if (thy_load.is_loaded(name.theory)) =>
- Exn.Exn(ERROR("Attempt to update loaded theory " + quote(name.theory)))
- case _ => header
- }
- (name, Document.Node.Header(header1))
+ val header1 =
+ if (thy_load.is_loaded(name.theory))
+ header.error("Attempt to update loaded theory " + quote(name.theory))
+ else header
+ (name, Document.Node.Deps(header1))
}
/* actor messages */
- private case class Start(args: List[String])
+ private case class Start(logic: String, args: List[String])
private case object Cancel_Execution
private case class Edit(edits: List[Document.Edit_Text])
private case class Change(
@@ -357,25 +354,16 @@
case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
System.err.println("cancel_scala " + id) // FIXME actually cancel JVM task
- case Isabelle_Markup.Ready if output.is_protocol =>
+ case _ if output.is_init =>
phase = Session.Ready
- case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
- thy_load.register_thy(name)
-
- case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol =>
- prover_syntax += (name, kind)
-
- case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
- prover_syntax += name
-
case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
if (rc == 0) phase = Session.Inactive
else phase = Session.Failed
- case _ =>
- if (output.is_init || output.is_stdout) { }
- else bad_output(output)
+ case _ if output.is_stdout =>
+
+ case _ => bad_output(output)
}
}
//}}}
@@ -389,9 +377,15 @@
receiveWithin(delay_commands_changed.flush_timeout) {
case TIMEOUT => delay_commands_changed.flush()
- case Start(args) if prover.isEmpty =>
+ case Start(name, args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
+
+ // FIXME static init in main constructor
+ val content = Build.session_content(name)
+ thy_load.register_thys(content.loaded_theories)
+ base_syntax = content.syntax
+
prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
}
@@ -446,7 +440,7 @@
/* actions */
- def start(args: List[String]) { session_actor ! Start(args) }
+ def start(name: String, args: List[String]) { session_actor ! Start(name, args) }
def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
@@ -456,7 +450,7 @@
{ session_actor !? Edit(edits) }
def init_node(name: Document.Node.Name,
- header: Document.Node_Header, perspective: Text.Perspective, text: String)
+ header: Document.Node.Header, perspective: Text.Perspective, text: String)
{
edit(List(header_edit(name, header),
name -> Document.Node.Clear(), // FIXME diff wrt. existing node
@@ -465,7 +459,7 @@
}
def edit_node(name: Document.Node.Name,
- header: Document.Node_Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
+ header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
{
edit(List(header_edit(name, header),
name -> Document.Node.Edits(text_edits),
--- a/src/Pure/Thy/thy_header.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_header.ML Tue Aug 07 22:32:14 2012 +0200
@@ -7,7 +7,8 @@
signature THY_HEADER =
sig
type header =
- {name: string, imports: string list,
+ {name: string,
+ imports: string list,
keywords: (string * Keyword.spec option) list,
uses: (Path.T * bool) list}
val make: string -> string list -> (string * Keyword.spec option) list ->
@@ -23,7 +24,8 @@
struct
type header =
- {name: string, imports: string list,
+ {name: string,
+ imports: string list,
keywords: (string * Keyword.spec option) list,
uses: (Path.T * bool) list};
--- a/src/Pure/Thy/thy_header.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala Tue Aug 07 22:32:14 2012 +0200
@@ -107,12 +107,17 @@
try { read(reader).map(Standard_System.decode_permissive_utf8) }
finally { reader.close }
}
+
+
+ /* keywords */
+
+ type Keywords = List[(String, Option[(String, List[String])])]
}
sealed case class Thy_Header(
name: String, imports: List[String],
- keywords: List[Outer_Syntax.Decl],
+ keywords: Thy_Header.Keywords,
uses: List[(String, Boolean)])
{
def map(f: String => String): Thy_Header =
--- a/src/Pure/Thy/thy_info.ML Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Aug 07 22:32:14 2012 +0200
@@ -10,7 +10,6 @@
datatype action = Update | Remove
val add_hook: (action -> string -> unit) -> unit
val get_names: unit -> string list
- val status: unit -> unit
val lookup_theory: string -> theory option
val get_theory: string -> theory
val is_finished: string -> bool
@@ -88,10 +87,6 @@
fun get_names () = Graph.topological_order (get_thys ());
-fun status () =
- List.app (fn name => Output.protocol_message (Isabelle_Markup.loaded_theory name) "")
- (get_names ());
-
(* access thy *)
--- a/src/Pure/Thy/thy_info.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala Tue Aug 07 22:32:14 2012 +0200
@@ -24,7 +24,7 @@
/* dependencies */
- type Dep = (Document.Node.Name, Document.Node_Header)
+ type Dep = (Document.Node.Name, Document.Node.Header)
private type Required = (List[Dep], Set[Document.Node.Name])
private def require_thys(initiators: List[Document.Node.Name],
@@ -40,7 +40,7 @@
else {
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
- val node_deps =
+ val header =
try { thy_load.check_thy(name) }
catch {
case ERROR(msg) =>
@@ -48,10 +48,13 @@
quote(name.theory) + required_by(initiators))
}
val (deps1, seen1) =
- require_thys(name :: initiators, (deps, seen + name), node_deps.imports)
- ((name, Exn.Res(node_deps)) :: deps1, seen1)
+ require_thys(name :: initiators, (deps, seen + name), header.imports)
+ ((name, header) :: deps1, seen1)
}
- catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) }
+ catch {
+ case e: Throwable =>
+ ((name, Document.Node.bad_header(Exn.message(e))) :: deps, seen + name)
+ }
}
}
--- a/src/Pure/Thy/thy_load.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala Tue Aug 07 22:32:14 2012 +0200
@@ -26,8 +26,11 @@
private var loaded_theories: Set[String] = preloaded
- def register_thy(thy_name: String): Unit =
- synchronized { loaded_theories += thy_name }
+ def register_thy(name: String): Unit =
+ synchronized { loaded_theories += name }
+
+ def register_thys(names: Set[String]): Unit =
+ synchronized { loaded_theories ++= names }
def is_loaded(thy_name: String): Boolean =
synchronized { loaded_theories.contains(thy_name) }
@@ -36,7 +39,7 @@
/* file-system operations */
def append(dir: String, source_path: Path): String =
- (Path.explode(dir) + source_path).implode
+ (Path.explode(dir) + source_path).expand.implode
def read_header(name: Document.Node.Name): Thy_Header =
{
@@ -60,7 +63,7 @@
}
}
- def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Deps =
+ def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Header =
{
val name1 = header.name
val imports = header.imports.map(import_name(name.dir, _))
@@ -69,10 +72,10 @@
if (name.theory != name1)
error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
" for theory " + quote(name1))
- Document.Node.Deps(imports, header.keywords, uses)
+ Document.Node.Header(imports, header.keywords, uses)
}
- def check_thy(name: Document.Node.Name): Document.Node.Deps =
+ def check_thy(name: Document.Node.Name): Document.Node.Header =
check_header(name, read_header(name))
}
--- a/src/Pure/Thy/thy_syntax.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Tue Aug 07 22:32:14 2012 +0200
@@ -33,7 +33,7 @@
def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
- List((0, "theory " + node_name.theory, buffer()))
+ List((0, node_name.theory, buffer()))
@tailrec def close(level: Int => Boolean)
{
@@ -134,26 +134,23 @@
val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
edits foreach {
- case (name, Document.Node.Header(header)) =>
+ case (name, Document.Node.Deps(header)) =>
val node = nodes(name)
val update_header =
- (node.header, header) match {
- case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
- case _ => true
- }
+ !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header
if (update_header) {
val node1 = node.update_header(header)
- updated_imports = updated_imports || (node.imports != node1.imports)
- updated_keywords = updated_keywords || (node.keywords != node1.keywords)
+ updated_imports = updated_imports || (node.header.imports != node1.header.imports)
+ updated_keywords = updated_keywords || (node.header.keywords != node1.header.keywords)
nodes += (name -> node1)
- doc_edits += (name -> Document.Node.Header(header))
+ doc_edits += (name -> Document.Node.Deps(header))
}
case _ =>
}
val syntax =
if (previous.is_init || updated_keywords)
- (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
+ (base_syntax /: nodes.entries) { case (syn, (_, node)) => syn.add_keywords(node.header) }
else previous.syntax
val reparse =
@@ -289,7 +286,7 @@
doc_edits += (name -> Document.Node.Edits(cmd_edits))
nodes += (name -> node.update_commands(commands3))
- case (name, Document.Node.Header(_)) =>
+ case (name, Document.Node.Deps(_)) =>
case (name, Document.Node.Perspective(text_perspective)) =>
val node = nodes(name)
--- a/src/Tools/jEdit/src/Isabelle.props Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Tue Aug 07 22:32:14 2012 +0200
@@ -67,9 +67,16 @@
isabelle-syslog.title=Syslog
#SideKick
-sidekick.parser.isabelle.label=Isabelle
+mode.isabelle-options.folding=sidekick
+mode.isabelle-options.sidekick.parser=isabelle-options
+mode.isabelle-root.folding=sidekick
+mode.isabelle-root.sidekick.parser=isabelle-root
+mode.isabelle.customSettings=true
+mode.isabelle.folding=sidekick
mode.isabelle.sidekick.parser=isabelle
+mode.isabelle.sidekick.showStatusWindow.label=true
mode.ml.sidekick.parser=isabelle
+sidekick.parser.isabelle.label=Isabelle
#Hyperlinks
mode.isabelle.hyperlink.source=isabelle
--- a/src/Tools/jEdit/src/document_model.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Tue Aug 07 22:32:14 2012 +0200
@@ -63,13 +63,16 @@
{
/* header */
- def node_header(): Document.Node_Header =
+ def node_header(): Document.Node.Header =
{
Swing_Thread.require()
Isabelle.buffer_lock(buffer) {
Exn.capture {
Isabelle.thy_load.check_header(name,
Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
+ } match {
+ case Exn.Res(header) => header
+ case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
}
}
}
--- a/src/Tools/jEdit/src/html_panel.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala Tue Aug 07 22:32:14 2012 +0200
@@ -134,7 +134,7 @@
val (font_metrics, margin) =
Swing_Thread.now {
val metrics = getFontMetrics(font)
- (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
+ (metrics, (getWidth() / (metrics.charWidth(Pretty.spc) max 1) - 4) max 20)
}
if (current_font_metrics == null ||
current_font_family != font_family ||
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 07 22:32:14 2012 +0200
@@ -48,14 +48,15 @@
}
-abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
+class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax])
+ extends SideKickParser(name)
{
/* parsing */
@volatile protected var stopped = false
override def stop() = { stopped = true }
- def parser(data: SideKickParsedData, model: Document_Model): Unit
+ def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
{
@@ -66,12 +67,16 @@
val root = data.root
data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
- Swing_Thread.now { Document_Model(buffer) } match {
- case Some(model) =>
- parser(data, model)
- if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
- case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
- }
+ val syntax = get_syntax
+ val ok =
+ if (syntax.isDefined) {
+ val ok = parser(buffer, syntax.get, data)
+ if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
+ else ok
+ }
+ else false
+ if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
+
data
}
@@ -87,15 +92,14 @@
val buffer = pane.getBuffer
Isabelle.buffer_lock(buffer) {
- Document_Model(buffer) match {
+ get_syntax match {
case None => null
- case Some(model) =>
+ case Some(syntax) =>
val line = buffer.getLineOfOffset(caret)
val start = buffer.getLineStartOffset(line)
val text = buffer.getSegment(start, caret - start)
- val completion = model.session.recent_syntax().completion
- completion.complete(text) match {
+ syntax.completion.complete(text) match {
case None => null
case Some((word, cs)) =>
val ds =
@@ -128,14 +132,16 @@
}
-class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
+class Isabelle_Sidekick_Structure(
+ name: String,
+ get_syntax: => Option[Outer_Syntax],
+ node_name: Buffer => Option[Document.Node.Name])
+ extends Isabelle_Sidekick(name, get_syntax)
{
import Thy_Syntax.Structure
- def parser(data: SideKickParsedData, model: Document_Model)
+ override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
- val syntax = model.session.recent_syntax()
-
def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
entry match {
case Structure.Block(name, body) =>
@@ -157,36 +163,57 @@
case _ => Nil
}
- val text = Isabelle.buffer_text(model.buffer)
- val structure = Structure.parse(syntax, model.name, text)
-
- make_tree(0, structure) foreach (node => data.root.add(node))
+ node_name(buffer) match {
+ case Some(name) =>
+ val text = Isabelle.buffer_text(buffer)
+ val structure = Structure.parse(syntax, name, text)
+ make_tree(0, structure) foreach (node => data.root.add(node))
+ true
+ case None => false
+ }
}
}
-class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
+class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
+ "isabelle", Isabelle.session.get_recent_syntax, Isabelle.buffer_node_name)
+
+
+class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
+ "isabelle-options", Some(Options.options_syntax), Isabelle.buffer_node_dummy)
+
+
+class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
+ "isabelle-root", Some(Build.root_syntax), Isabelle.buffer_node_dummy)
+
+
+class Isabelle_Sidekick_Raw
+ extends Isabelle_Sidekick("isabelle-raw", Isabelle.session.get_recent_syntax)
{
- def parser(data: SideKickParsedData, model: Document_Model)
+ override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
- val root = data.root
- val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
- for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
- snapshot.state.command_state(snapshot.version, command).markup
- .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
- {
- val range = info.range + command_start
- val content = command.source(info.range).replace('\n', ' ')
- val info_text =
- Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
+ Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
+ case Some(snapshot) =>
+ val root = data.root
+ for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
+ snapshot.state.command_state(snapshot.version, command).markup
+ .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
+ {
+ val range = info.range + command_start
+ val content = command.source(info.range).replace('\n', ' ')
+ val info_text =
+ Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
- new DefaultMutableTreeNode(
- 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
+ new DefaultMutableTreeNode(
+ 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
+ })
})
- })
+ }
+ true
+ case None => false
}
}
}
--- a/src/Tools/jEdit/src/jEdit.props Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Tue Aug 07 22:32:14 2012 +0200
@@ -180,14 +180,11 @@
isabelle-output.dock-position=bottom
isabelle-output.height=174
isabelle-output.width=412
+isabelle-readme.dock-position=bottom
isabelle-session.dock-position=bottom
-isabelle-readme.dock-position=bottom
line-end.shortcut=END
line-home.shortcut=HOME
lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
-mode.isabelle.customSettings=true
-mode.isabelle.folding=sidekick
-mode.isabelle.sidekick.showStatusWindow.label=true
print.font=IsabelleText
restore.remote=false
restore=false
--- a/src/Tools/jEdit/src/modes/isabelle-options.xml Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-options.xml Tue Aug 07 22:32:14 2012 +0200
@@ -4,34 +4,10 @@
<!-- Isabelle options mode -->
<MODE>
<PROPS>
- <PROPERTY NAME="commentStart" VALUE="(*"/>
- <PROPERTY NAME="commentEnd" VALUE="*)"/>
<PROPERTY NAME="noWordSep" VALUE="_'.?"/>
<PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
<PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
<PROPERTY NAME="tabSize" VALUE="2" />
<PROPERTY NAME="indentSize" VALUE="2" />
</PROPS>
- <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
- <SPAN TYPE="COMMENT1">
- <BEGIN>(*</BEGIN>
- <END>*)</END>
- </SPAN>
- <SPAN TYPE="COMMENT3">
- <BEGIN>{*</BEGIN>
- <END>*}</END>
- </SPAN>
- <SPAN TYPE="LITERAL2">
- <BEGIN>`</BEGIN>
- <END>`</END>
- </SPAN>
- <SPAN TYPE="LITERAL1">
- <BEGIN>"</BEGIN>
- <END>"</END>
- </SPAN>
- <KEYWORDS>
- <KEYWORD1>declare</KEYWORD1>
- <KEYWORD2>define</KEYWORD2>
- </KEYWORDS>
- </RULES>
</MODE>
--- a/src/Tools/jEdit/src/modes/isabelle-root.xml Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-root.xml Tue Aug 07 22:32:14 2012 +0200
@@ -4,38 +4,10 @@
<!-- Isabelle session root mode -->
<MODE>
<PROPS>
- <PROPERTY NAME="commentStart" VALUE="(*"/>
- <PROPERTY NAME="commentEnd" VALUE="*)"/>
<PROPERTY NAME="noWordSep" VALUE="_'.?"/>
<PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
<PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
<PROPERTY NAME="tabSize" VALUE="2" />
<PROPERTY NAME="indentSize" VALUE="2" />
</PROPS>
- <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
- <SPAN TYPE="COMMENT1">
- <BEGIN>(*</BEGIN>
- <END>*)</END>
- </SPAN>
- <SPAN TYPE="COMMENT3">
- <BEGIN>{*</BEGIN>
- <END>*}</END>
- </SPAN>
- <SPAN TYPE="LITERAL2">
- <BEGIN>`</BEGIN>
- <END>`</END>
- </SPAN>
- <SPAN TYPE="LITERAL1">
- <BEGIN>"</BEGIN>
- <END>"</END>
- </SPAN>
- <KEYWORDS>
- <KEYWORD1>session</KEYWORD1>
- <KEYWORD2>in</KEYWORD2>
- <KEYWORD2>description</KEYWORD2>
- <KEYWORD2>files</KEYWORD2>
- <KEYWORD2>options</KEYWORD2>
- <KEYWORD2>theories</KEYWORD2>
- </KEYWORDS>
- </RULES>
</MODE>
--- a/src/Tools/jEdit/src/plugin.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 07 22:32:14 2012 +0200
@@ -147,6 +147,15 @@
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+ def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
+ Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
+
+ def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
+ {
+ val name = buffer_name(buffer)
+ Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
+ }
+
/* main jEdit components */
@@ -197,18 +206,14 @@
{
swing_buffer_lock(buffer) {
val opt_model =
- {
- val name = buffer_name(buffer)
- Thy_Header.thy_name(name) match {
- case Some(theory) =>
- val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
+ buffer_node_name(buffer) match {
+ case Some(node_name) =>
document_model(buffer) match {
case Some(model) if model.name == node_name => Some(model)
case _ => Some(Document_Model.init(session, buffer, node_name))
}
case None => None
}
- }
if (opt_model.isDefined) {
for (text_area <- jedit_text_areas(buffer)) {
if (document_view(text_area).map(_.model) != opt_model)
@@ -301,7 +306,8 @@
if (logic != null && logic != "") logic
else Isabelle.default_logic()
}
- session.start(modes ::: List(logic))
+ val name = Path.explode(logic).base.implode // FIXME more robust session name
+ session.start(name, modes ::: List(logic))
}
--- a/src/Tools/jEdit/src/services.xml Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/services.xml Tue Aug 07 22:32:14 2012 +0200
@@ -8,6 +8,12 @@
<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
new isabelle.jedit.Isabelle_Sidekick_Default();
</SERVICE>
+ <SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick_Options();
+ </SERVICE>
+ <SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick_Root();
+ </SERVICE>
<SERVICE NAME="isabelle-raw" CLASS="sidekick.SideKickParser">
new isabelle.jedit.Isabelle_Sidekick_Raw();
</SERVICE>
--- a/src/Tools/jEdit/src/token_markup.scala Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Tue Aug 07 22:32:14 2012 +0200
@@ -162,7 +162,7 @@
}
}
- class Marker extends TokenMarker
+ class Marker(ext_styles: Boolean, get_syntax: => Option[Outer_Syntax]) extends TokenMarker
{
override def markTokens(context: TokenMarker.LineContext,
handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
@@ -176,12 +176,12 @@
val context1 =
{
+ val syntax = get_syntax
val (styled_tokens, context1) =
- if (line_ctxt.isDefined && Isabelle.session.is_ready) {
- val syntax = Isabelle.session.recent_syntax()
- val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
+ if (line_ctxt.isDefined && syntax.isDefined) {
+ val (tokens, ctxt1) = syntax.get.scan_context(line, line_ctxt.get)
val styled_tokens =
- tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))
+ tokens.map(tok => (Isabelle_Rendering.token_markup(syntax.get, tok), tok))
(styled_tokens, new Line_Context(Some(ctxt1)))
}
else {
@@ -189,7 +189,9 @@
(List((JEditToken.NULL, token)), new Line_Context(None))
}
- val extended = extended_styles(line)
+ val extended =
+ if (ext_styles) extended_styles(line)
+ else Map.empty[Text.Offset, Byte => Byte]
var offset = 0
for ((style, token) <- styled_tokens) {
@@ -221,7 +223,10 @@
/* mode provider */
- private val isabelle_token_marker = new Token_Markup.Marker
+ private val markers = Map(
+ "isabelle" -> new Token_Markup.Marker(true, Isabelle.session.get_recent_syntax()),
+ "isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
+ "isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))
class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
{
@@ -230,15 +235,14 @@
override def loadMode(mode: Mode, xmh: XModeHandler)
{
super.loadMode(mode, xmh)
- if (mode.getName == "isabelle")
- mode.setTokenMarker(isabelle_token_marker)
+ markers.get(mode.getName).map(mode.setTokenMarker(_))
}
}
def refresh_buffer(buffer: JEditBuffer)
{
buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
- buffer.setTokenMarker(isabelle_token_marker)
+ markers.get(buffer.getMode.getName).map(buffer.setTokenMarker(_))
}
}