treat sessions as entities with defining position;
authorwenzelm
Tue Jan 23 19:25:39 2018 +0100 (16 months ago)
changeset 67493c4e9e0c50487
parent 67492 954f44210b92
child 67494 b8e093f7a802
treat sessions as entities with defining position;
tuned signature;
src/Pure/ML/ml_process.scala
src/Pure/ML/ml_syntax.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.ML
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/ML/ml_process.scala	Tue Jan 23 17:58:09 2018 +0100
     1.2 +++ b/src/Pure/ML/ml_process.scala	Tue Jan 23 19:25:39 2018 +0100
     1.3 @@ -101,8 +101,12 @@
     1.4                  ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
     1.5            def print_list(list: List[String]): String =
     1.6              ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
     1.7 +          def print_sessions(list: List[(String, Position.T)]): String =
     1.8 +            ML_Syntax.print_list(
     1.9 +              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
    1.10 +
    1.11            List("Resources.init_session_base" +
    1.12 -            " {sessions = " + print_list(base.known.sessions.toList) +
    1.13 +            " {sessions = " + print_sessions(base.known.sessions.toList) +
    1.14              ", doc_names = " + print_list(base.doc_names) +
    1.15              ", global_theories = " + print_table(base.global_theories.toList) +
    1.16              ", loaded_theories = " + print_list(base.loaded_theories.keys) +
     2.1 --- a/src/Pure/ML/ml_syntax.scala	Tue Jan 23 17:58:09 2018 +0100
     2.2 +++ b/src/Pure/ML/ml_syntax.scala	Tue Jan 23 19:25:39 2018 +0100
     2.3 @@ -56,4 +56,10 @@
     2.4  
     2.5    def print_list[A](f: A => String)(list: List[A]): String =
     2.6      "[" + commas(list.map(f)) + "]"
     2.7 +
     2.8 +
     2.9 +  /* properties */
    2.10 +
    2.11 +  def print_properties(props: Properties.T): String =
    2.12 +    print_list(print_pair(print_string_bytes(_), print_string_bytes(_))(_))(props)
    2.13  }
     3.1 --- a/src/Pure/PIDE/protocol.ML	Tue Jan 23 17:58:09 2018 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Jan 23 19:25:39 2018 +0100
     3.3 @@ -24,10 +24,12 @@
     3.4        let
     3.5          val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
     3.6          val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
     3.7 +        val decode_sessions =
     3.8 +          YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
     3.9        in
    3.10          Resources.init_session_base
    3.11 -          {sessions = decode_list sessions_yxml,
    3.12 -           doc_names = decode_list doc_names_yxml,
    3.13 +          {sessions = decode_sessions sessions_yxml,
    3.14 +           docs = decode_list doc_names_yxml,
    3.15             global_theories = decode_table global_theories_yxml,
    3.16             loaded_theories = decode_list loaded_theories_yxml,
    3.17             known_theories = decode_table known_theories_yxml}
     4.1 --- a/src/Pure/PIDE/protocol.scala	Tue Jan 23 17:58:09 2018 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Jan 23 19:25:39 2018 +0100
     4.3 @@ -338,11 +338,17 @@
     4.4      Symbol.encode_yxml(list(string)(lst))
     4.5    }
     4.6  
     4.7 +  private def encode_sessions(lst: List[(String, Position.T)]): String =
     4.8 +  {
     4.9 +    import XML.Encode._
    4.10 +    Symbol.encode_yxml(list(pair(string, properties))(lst))
    4.11 +  }
    4.12 +
    4.13    def session_base(resources: Resources)
    4.14    {
    4.15      val base = resources.session_base.standard_path
    4.16      protocol_command("Prover.init_session_base",
    4.17 -      encode_list(base.known.sessions.toList),
    4.18 +      encode_sessions(base.known.sessions.toList),
    4.19        encode_list(base.doc_names),
    4.20        encode_table(base.global_theories.toList),
    4.21        encode_list(base.loaded_theories.keys),
     5.1 --- a/src/Pure/PIDE/resources.ML	Tue Jan 23 17:58:09 2018 +0100
     5.2 +++ b/src/Pure/PIDE/resources.ML	Tue Jan 23 19:25:39 2018 +0100
     5.3 @@ -8,8 +8,8 @@
     5.4  sig
     5.5    val default_qualifier: string
     5.6    val init_session_base:
     5.7 -    {sessions: string list,
     5.8 -     doc_names: string list,
     5.9 +    {sessions: (string * Properties.T) list,
    5.10 +     docs: string list,
    5.11       global_theories: (string * string) list,
    5.12       loaded_theories: string list,
    5.13       known_theories: (string * string) list} -> unit
    5.14 @@ -45,9 +45,14 @@
    5.15  
    5.16  val default_qualifier = "Draft";
    5.17  
    5.18 +type entry = {pos: Position.T, serial: serial};
    5.19 +
    5.20 +fun make_entry props : entry =
    5.21 +  {pos = Position.of_properties props, serial = serial ()};
    5.22 +
    5.23  val empty_session_base =
    5.24 -  {sessions = []: string list,
    5.25 -   doc_names = []: string list,
    5.26 +  {sessions = []: (string * entry) list,
    5.27 +   docs = []: (string * entry) list,
    5.28     global_theories = Symtab.empty: string Symtab.table,
    5.29     loaded_theories = Symtab.empty: unit Symtab.table,
    5.30     known_theories = Symtab.empty: Path.T Symtab.table};
    5.31 @@ -55,11 +60,11 @@
    5.32  val global_session_base =
    5.33    Synchronized.var "Sessions.base" empty_session_base;
    5.34  
    5.35 -fun init_session_base {sessions, doc_names, global_theories, loaded_theories, known_theories} =
    5.36 +fun init_session_base {sessions, docs, global_theories, loaded_theories, known_theories} =
    5.37    Synchronized.change global_session_base
    5.38      (fn _ =>
    5.39 -      {sessions = sort_strings sessions,
    5.40 -       doc_names = doc_names,
    5.41 +      {sessions = sort_by #1 (map (apsnd make_entry) sessions),
    5.42 +       docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
    5.43         global_theories = Symtab.make global_theories,
    5.44         loaded_theories = Symtab.make_set loaded_theories,
    5.45         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    5.46 @@ -68,7 +73,7 @@
    5.47    Synchronized.change global_session_base
    5.48      (fn {global_theories, loaded_theories, ...} =>
    5.49        {sessions = [],
    5.50 -       doc_names = [],
    5.51 +       docs = [],
    5.52         global_theories = global_theories,
    5.53         loaded_theories = loaded_theories,
    5.54         known_theories = #known_theories empty_session_base});
    5.55 @@ -80,23 +85,28 @@
    5.56  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    5.57  
    5.58  fun check_name which kind markup ctxt (name, pos) =
    5.59 -  let val names = get_session_base which in
    5.60 -    if member (op =) names name then
    5.61 -      (Context_Position.report ctxt pos (markup name); name)
    5.62 -    else
    5.63 -      let
    5.64 -        val completion =
    5.65 -          Completion.make (name, pos) (fn completed =>
    5.66 -              names
    5.67 -              |> filter completed
    5.68 -              |> sort_strings
    5.69 -              |> map (fn a => (a, (kind, a))));
    5.70 -        val report = Markup.markup_report (Completion.reported_text completion);
    5.71 -      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end
    5.72 +  let val entries = get_session_base which in
    5.73 +    (case AList.lookup (op =) entries name of
    5.74 +      SOME entry => (Context_Position.report ctxt pos (markup name entry); name)
    5.75 +    | NONE =>
    5.76 +        let
    5.77 +          val completion =
    5.78 +            Completion.make (name, pos) (fn completed =>
    5.79 +                entries
    5.80 +                |> map #1
    5.81 +                |> filter completed
    5.82 +                |> sort_strings
    5.83 +                |> map (fn a => (a, (kind, a))));
    5.84 +          val report = Markup.markup_report (Completion.reported_text completion);
    5.85 +        in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end)
    5.86    end;
    5.87  
    5.88 -val check_session = check_name #sessions "session" (Markup.entity Markup.sessionN);
    5.89 -val check_doc = check_name #doc_names "documentation" Markup.doc;
    5.90 +fun markup_session name {pos, serial} =
    5.91 +  Markup.properties
    5.92 +    (Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name);
    5.93 +
    5.94 +val check_session = check_name #sessions "session" markup_session;
    5.95 +val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name);
    5.96  
    5.97  
    5.98  
     6.1 --- a/src/Pure/Thy/sessions.scala	Tue Jan 23 17:58:09 2018 +0100
     6.2 +++ b/src/Pure/Thy/sessions.scala	Tue Jan 23 19:25:39 2018 +0100
     6.3 @@ -40,7 +40,7 @@
     6.4      val empty: Known = Known()
     6.5  
     6.6      def make(local_dir: Path, bases: List[Base],
     6.7 -      sessions: List[String] = Nil,
     6.8 +      sessions: List[(String, Position.T)] = Nil,
     6.9        theories: List[Document.Node.Name] = Nil,
    6.10        loaded_files: List[(String, List[Path])] = Nil): Known =
    6.11      {
    6.12 @@ -57,7 +57,7 @@
    6.13        }
    6.14  
    6.15        val known_sessions =
    6.16 -        (sessions.toSet /: bases)({ case (known, base) => known ++ base.known.sessions })
    6.17 +        (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
    6.18  
    6.19        val known_theories =
    6.20          (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
    6.21 @@ -96,7 +96,7 @@
    6.22    }
    6.23  
    6.24    sealed case class Known(
    6.25 -    sessions: Set[String] = Set.empty,
    6.26 +    sessions: Map[String, Position.T] = Map.empty,
    6.27      theories: Map[String, Document.Node.Name] = Map.empty,
    6.28      theories_local: Map[String, Document.Node.Name] = Map.empty,
    6.29      files: Map[JFile, List[Document.Node.Name]] = Map.empty,
    6.30 @@ -317,7 +317,7 @@
    6.31  
    6.32              val known =
    6.33                Known.make(info.dir, List(imports_base),
    6.34 -                sessions = List(info.name),
    6.35 +                sessions = List(info.name -> info.pos),
    6.36                  theories = dependencies.theories,
    6.37                  loaded_files = loaded_files)
    6.38  
     7.1 --- a/src/Pure/Tools/build.ML	Tue Jan 23 17:58:09 2018 +0100
     7.2 +++ b/src/Pure/Tools/build.ML	Tue Jan 23 19:25:39 2018 +0100
     7.3 @@ -149,7 +149,7 @@
     7.4    name: string,
     7.5    master_dir: Path.T,
     7.6    theories: (Options.T * (string * Position.T) list) list,
     7.7 -  sessions: string list,
     7.8 +  sessions: (string * Properties.T) list,
     7.9    doc_names: string list,
    7.10    global_theories: (string * string) list,
    7.11    loaded_theories: string list,
    7.12 @@ -168,8 +168,9 @@
    7.13          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    7.14            (pair string
    7.15              (pair (((list (pair Options.decode (list (pair string position))))))
    7.16 -              (pair (list string) (pair (list string) (pair (list (pair string string)) (pair (list string)
    7.17 -                (pair (list (pair string string)) (list string)))))))))))))))))
    7.18 +              (pair (list (pair string properties)) (pair (list string)
    7.19 +                (pair (list (pair string string)) (pair (list string)
    7.20 +                  (pair (list (pair string string)) (list string)))))))))))))))))
    7.21        (YXML.parse_body yxml);
    7.22    in
    7.23      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
    7.24 @@ -190,7 +191,7 @@
    7.25      val _ =
    7.26        Resources.init_session_base
    7.27          {sessions = sessions,
    7.28 -         doc_names = doc_names,
    7.29 +         docs = doc_names,
    7.30           global_theories = global_theories,
    7.31           loaded_theories = loaded_theories,
    7.32           known_theories = known_theories};
     8.1 --- a/src/Pure/Tools/build.scala	Tue Jan 23 17:58:09 2018 +0100
     8.2 +++ b/src/Pure/Tools/build.scala	Tue Jan 23 19:25:39 2018 +0100
     8.3 @@ -212,7 +212,8 @@
     8.4                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
     8.5                  pair(string, pair(string, pair(string, pair(Path.encode,
     8.6                  pair(list(pair(Options.encode, list(pair(string, properties)))),
     8.7 -                pair(list(string), pair(list(string), pair(list(pair(string, string)),
     8.8 +                pair(list(pair(string, properties)), pair(list(string),
     8.9 +                pair(list(pair(string, string)),
    8.10                  pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
    8.11                (Symbol.codes, (command_timings, (do_output, (verbose,
    8.12                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),