--- a/src/Pure/ML/ml_process.scala Tue Jan 23 17:58:09 2018 +0100
+++ b/src/Pure/ML/ml_process.scala Tue Jan 23 19:25:39 2018 +0100
@@ -101,8 +101,12 @@
ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
def print_list(list: List[String]): String =
ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
+ def print_sessions(list: List[(String, Position.T)]): String =
+ ML_Syntax.print_list(
+ ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
+
List("Resources.init_session_base" +
- " {sessions = " + print_list(base.known.sessions.toList) +
+ " {sessions = " + print_sessions(base.known.sessions.toList) +
", doc_names = " + print_list(base.doc_names) +
", global_theories = " + print_table(base.global_theories.toList) +
", loaded_theories = " + print_list(base.loaded_theories.keys) +
--- a/src/Pure/ML/ml_syntax.scala Tue Jan 23 17:58:09 2018 +0100
+++ b/src/Pure/ML/ml_syntax.scala Tue Jan 23 19:25:39 2018 +0100
@@ -56,4 +56,10 @@
def print_list[A](f: A => String)(list: List[A]): String =
"[" + commas(list.map(f)) + "]"
+
+
+ /* properties */
+
+ def print_properties(props: Properties.T): String =
+ print_list(print_pair(print_string_bytes(_), print_string_bytes(_))(_))(props)
}
--- a/src/Pure/PIDE/protocol.ML Tue Jan 23 17:58:09 2018 +0100
+++ b/src/Pure/PIDE/protocol.ML Tue Jan 23 19:25:39 2018 +0100
@@ -24,10 +24,12 @@
let
val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
+ val decode_sessions =
+ YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
in
Resources.init_session_base
- {sessions = decode_list sessions_yxml,
- doc_names = decode_list doc_names_yxml,
+ {sessions = decode_sessions sessions_yxml,
+ docs = decode_list doc_names_yxml,
global_theories = decode_table global_theories_yxml,
loaded_theories = decode_list loaded_theories_yxml,
known_theories = decode_table known_theories_yxml}
--- a/src/Pure/PIDE/protocol.scala Tue Jan 23 17:58:09 2018 +0100
+++ b/src/Pure/PIDE/protocol.scala Tue Jan 23 19:25:39 2018 +0100
@@ -338,11 +338,17 @@
Symbol.encode_yxml(list(string)(lst))
}
+ private def encode_sessions(lst: List[(String, Position.T)]): String =
+ {
+ import XML.Encode._
+ Symbol.encode_yxml(list(pair(string, properties))(lst))
+ }
+
def session_base(resources: Resources)
{
val base = resources.session_base.standard_path
protocol_command("Prover.init_session_base",
- encode_list(base.known.sessions.toList),
+ encode_sessions(base.known.sessions.toList),
encode_list(base.doc_names),
encode_table(base.global_theories.toList),
encode_list(base.loaded_theories.keys),
--- a/src/Pure/PIDE/resources.ML Tue Jan 23 17:58:09 2018 +0100
+++ b/src/Pure/PIDE/resources.ML Tue Jan 23 19:25:39 2018 +0100
@@ -8,8 +8,8 @@
sig
val default_qualifier: string
val init_session_base:
- {sessions: string list,
- doc_names: string list,
+ {sessions: (string * Properties.T) list,
+ docs: string list,
global_theories: (string * string) list,
loaded_theories: string list,
known_theories: (string * string) list} -> unit
@@ -45,9 +45,14 @@
val default_qualifier = "Draft";
+type entry = {pos: Position.T, serial: serial};
+
+fun make_entry props : entry =
+ {pos = Position.of_properties props, serial = serial ()};
+
val empty_session_base =
- {sessions = []: string list,
- doc_names = []: string list,
+ {sessions = []: (string * entry) list,
+ docs = []: (string * entry) list,
global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: unit Symtab.table,
known_theories = Symtab.empty: Path.T Symtab.table};
@@ -55,11 +60,11 @@
val global_session_base =
Synchronized.var "Sessions.base" empty_session_base;
-fun init_session_base {sessions, doc_names, global_theories, loaded_theories, known_theories} =
+fun init_session_base {sessions, docs, global_theories, loaded_theories, known_theories} =
Synchronized.change global_session_base
(fn _ =>
- {sessions = sort_strings sessions,
- doc_names = doc_names,
+ {sessions = sort_by #1 (map (apsnd make_entry) sessions),
+ docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make_set loaded_theories,
known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
@@ -68,7 +73,7 @@
Synchronized.change global_session_base
(fn {global_theories, loaded_theories, ...} =>
{sessions = [],
- doc_names = [],
+ docs = [],
global_theories = global_theories,
loaded_theories = loaded_theories,
known_theories = #known_theories empty_session_base});
@@ -80,23 +85,28 @@
fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
fun check_name which kind markup ctxt (name, pos) =
- let val names = get_session_base which in
- if member (op =) names name then
- (Context_Position.report ctxt pos (markup name); name)
- else
- let
- val completion =
- Completion.make (name, pos) (fn completed =>
- names
- |> filter completed
- |> sort_strings
- |> map (fn a => (a, (kind, a))));
- val report = Markup.markup_report (Completion.reported_text completion);
- in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end
+ let val entries = get_session_base which in
+ (case AList.lookup (op =) entries name of
+ SOME entry => (Context_Position.report ctxt pos (markup name entry); name)
+ | NONE =>
+ let
+ val completion =
+ Completion.make (name, pos) (fn completed =>
+ entries
+ |> map #1
+ |> filter completed
+ |> sort_strings
+ |> map (fn a => (a, (kind, a))));
+ val report = Markup.markup_report (Completion.reported_text completion);
+ in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end)
end;
-val check_session = check_name #sessions "session" (Markup.entity Markup.sessionN);
-val check_doc = check_name #doc_names "documentation" Markup.doc;
+fun markup_session name {pos, serial} =
+ Markup.properties
+ (Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name);
+
+val check_session = check_name #sessions "session" markup_session;
+val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name);
--- a/src/Pure/Thy/sessions.scala Tue Jan 23 17:58:09 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Jan 23 19:25:39 2018 +0100
@@ -40,7 +40,7 @@
val empty: Known = Known()
def make(local_dir: Path, bases: List[Base],
- sessions: List[String] = Nil,
+ sessions: List[(String, Position.T)] = Nil,
theories: List[Document.Node.Name] = Nil,
loaded_files: List[(String, List[Path])] = Nil): Known =
{
@@ -57,7 +57,7 @@
}
val known_sessions =
- (sessions.toSet /: bases)({ case (known, base) => known ++ base.known.sessions })
+ (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
val known_theories =
(Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
@@ -96,7 +96,7 @@
}
sealed case class Known(
- sessions: Set[String] = Set.empty,
+ sessions: Map[String, Position.T] = Map.empty,
theories: Map[String, Document.Node.Name] = Map.empty,
theories_local: Map[String, Document.Node.Name] = Map.empty,
files: Map[JFile, List[Document.Node.Name]] = Map.empty,
@@ -317,7 +317,7 @@
val known =
Known.make(info.dir, List(imports_base),
- sessions = List(info.name),
+ sessions = List(info.name -> info.pos),
theories = dependencies.theories,
loaded_files = loaded_files)
--- a/src/Pure/Tools/build.ML Tue Jan 23 17:58:09 2018 +0100
+++ b/src/Pure/Tools/build.ML Tue Jan 23 19:25:39 2018 +0100
@@ -149,7 +149,7 @@
name: string,
master_dir: Path.T,
theories: (Options.T * (string * Position.T) list) list,
- sessions: string list,
+ sessions: (string * Properties.T) list,
doc_names: string list,
global_theories: (string * string) list,
loaded_theories: string list,
@@ -168,8 +168,9 @@
(pair (list (pair string string)) (pair string (pair string (pair string (pair string
(pair string
(pair (((list (pair Options.decode (list (pair string position))))))
- (pair (list string) (pair (list string) (pair (list (pair string string)) (pair (list string)
- (pair (list (pair string string)) (list string)))))))))))))))))
+ (pair (list (pair string properties)) (pair (list string)
+ (pair (list (pair string string)) (pair (list string)
+ (pair (list (pair string string)) (list string)))))))))))))))))
(YXML.parse_body yxml);
in
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
@@ -190,7 +191,7 @@
val _ =
Resources.init_session_base
{sessions = sessions,
- doc_names = doc_names,
+ docs = doc_names,
global_theories = global_theories,
loaded_theories = loaded_theories,
known_theories = known_theories};
--- a/src/Pure/Tools/build.scala Tue Jan 23 17:58:09 2018 +0100
+++ b/src/Pure/Tools/build.scala Tue Jan 23 19:25:39 2018 +0100
@@ -212,7 +212,8 @@
pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
pair(string, pair(string, pair(string, pair(Path.encode,
pair(list(pair(Options.encode, list(pair(string, properties)))),
- pair(list(string), pair(list(string), pair(list(pair(string, string)),
+ pair(list(pair(string, properties)), pair(list(string),
+ pair(list(pair(string, string)),
pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
(Symbol.codes, (command_timings, (do_output, (verbose,
(store.browser_info, (info.document_files, (File.standard_path(graph_file),