# HG changeset patch # User wenzelm # Date 1516731939 -3600 # Node ID c4e9e0c50487075f296a1bef1f5cf628cc1b459d # Parent 954f44210b9250001d58eea75647aa06df721137 treat sessions as entities with defining position; tuned signature; diff -r 954f44210b92 -r c4e9e0c50487 src/Pure/ML/ml_process.scala --- 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) + diff -r 954f44210b92 -r c4e9e0c50487 src/Pure/ML/ml_syntax.scala --- 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) } diff -r 954f44210b92 -r c4e9e0c50487 src/Pure/PIDE/protocol.ML --- 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} diff -r 954f44210b92 -r c4e9e0c50487 src/Pure/PIDE/protocol.scala --- 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), diff -r 954f44210b92 -r c4e9e0c50487 src/Pure/PIDE/resources.ML --- 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); diff -r 954f44210b92 -r c4e9e0c50487 src/Pure/Thy/sessions.scala --- 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) diff -r 954f44210b92 -r c4e9e0c50487 src/Pure/Tools/build.ML --- 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}; diff -r 954f44210b92 -r c4e9e0c50487 src/Pure/Tools/build.scala --- 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),