PIDE markup for session ROOT files;
authorwenzelm
Sat Dec 16 16:46:01 2017 +0100 (21 months ago ago)
changeset 6721503d0c958d65a
parent 67214 87038a574d09
child 67216 99815211970c
PIDE markup for session ROOT files;
NEWS
src/Doc/ROOT
src/HOL/ROOT
src/Pure/Isar/parse.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Sessions.thy
src/Pure/Thy/sessions.ML
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_header.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/NEWS	Sat Dec 16 15:15:51 2017 +0100
     1.2 +++ b/NEWS	Sat Dec 16 16:46:01 2017 +0100
     1.3 @@ -44,6 +44,8 @@
     1.4  
     1.5  *** Prover IDE -- Isabelle/Scala/jEdit ***
     1.6  
     1.7 +* PIDE markup for session ROOT files.
     1.8 +
     1.9  * Completion supports theory header imports, using theory base name.
    1.10  E.g. "Prob" may be completed to "HOL-Probability.Probability".
    1.11  
     2.1 --- a/src/Doc/ROOT	Sat Dec 16 15:15:51 2017 +0100
     2.2 +++ b/src/Doc/ROOT	Sat Dec 16 16:46:01 2017 +0100
     2.3 @@ -148,7 +148,7 @@
     2.4      Integration
     2.5      Isar
     2.6      Local_Theory
     2.7 -    ML
     2.8 +    "ML"
     2.9      Prelim
    2.10      Proof
    2.11      Syntax
     3.1 --- a/src/HOL/ROOT	Sat Dec 16 15:15:51 2017 +0100
     3.2 +++ b/src/HOL/ROOT	Sat Dec 16 16:46:01 2017 +0100
     3.3 @@ -558,7 +558,7 @@
     3.4      Lagrange
     3.5      List_to_Set_Comprehension_Examples
     3.6      LocaleTest2
     3.7 -    ML
     3.8 +    "ML"
     3.9      MergeSort
    3.10      MonoidGroup
    3.11      Multiquote
     4.1 --- a/src/Pure/Isar/parse.ML	Sat Dec 16 15:15:51 2017 +0100
     4.2 +++ b/src/Pure/Isar/parse.ML	Sat Dec 16 16:46:01 2017 +0100
     4.3 @@ -67,6 +67,7 @@
     4.4    val embedded: string parser
     4.5    val text: string parser
     4.6    val path: string parser
     4.7 +  val session_name: string parser
     4.8    val theory_name: string parser
     4.9    val liberal_name: string parser
    4.10    val parname: string parser
    4.11 @@ -109,6 +110,9 @@
    4.12    val thm_sel: Facts.interval list parser
    4.13    val thm: (Facts.ref * Token.src list) parser
    4.14    val thms1: (Facts.ref * Token.src list) list parser
    4.15 +  val option_name: string parser
    4.16 +  val option_value: string parser
    4.17 +  val options: ((string * Position.T) * (string * Position.T)) list parser
    4.18  end;
    4.19  
    4.20  structure Parse: PARSE =
    4.21 @@ -272,6 +276,7 @@
    4.22  
    4.23  val path = group (fn () => "file name/path specification") embedded;
    4.24  
    4.25 +val session_name = group (fn () => "session name") name;
    4.26  val theory_name = group (fn () => "theory name") name;
    4.27  
    4.28  val liberal_name = keyword_with Token.ident_or_symbolic || name;
    4.29 @@ -466,4 +471,16 @@
    4.30  
    4.31  val thms1 = Scan.repeat1 thm;
    4.32  
    4.33 +
    4.34 +(* options *)
    4.35 +
    4.36 +val option_name = group (fn () => "option name") name;
    4.37 +val option_value = group (fn () => "option value") ((token real || token name) >> Token.content_of);
    4.38 +
    4.39 +val option =
    4.40 +  position option_name :-- (fn (_, pos) =>
    4.41 +    Scan.optional ($$$ "=" |-- !!! (position option_value)) ("true", pos));
    4.42 +
    4.43 +val options = $$$ "[" |-- list1 option --| $$$ "]";
    4.44 +
    4.45  end;
     5.1 --- a/src/Pure/PIDE/document.ML	Sat Dec 16 15:15:51 2017 +0100
     5.2 +++ b/src/Pure/PIDE/document.ML	Sat Dec 16 16:46:01 2017 +0100
     5.3 @@ -578,14 +578,18 @@
     5.4      val _ = Position.reports (map #2 parents_reports);
     5.5    in Resources.begin_theory master_dir header parents end;
     5.6  
     5.7 -fun check_ml_root node =
     5.8 -  if member (op =) Thy_Header.ml_roots (#1 (#name (#header (get_header node)))) then
     5.9 -    let
    5.10 -      val master_dir = master_directory node;
    5.11 -      val header = #header (get_header node);
    5.12 -      val parent = Thy_Info.get_theory Thy_Header.ml_bootstrapN;
    5.13 -    in SOME (Resources.begin_theory master_dir header [parent]) end
    5.14 -  else NONE;
    5.15 +fun check_root_theory node =
    5.16 +  let
    5.17 +    val master_dir = master_directory node;
    5.18 +    val header = #header (get_header node);
    5.19 +    val header_name = #1 (#name header);
    5.20 +    val parent =
    5.21 +      if header_name = Sessions.root_name then
    5.22 +        SOME (Thy_Info.get_theory Sessions.theory_name)
    5.23 +      else if member (op =) Thy_Header.ml_roots header_name then
    5.24 +        SOME (Thy_Info.get_theory Thy_Header.ml_bootstrapN)
    5.25 +      else NONE;
    5.26 +  in parent |> Option.map (fn thy => Resources.begin_theory master_dir header [thy]) end;
    5.27  
    5.28  fun check_theory full name node =
    5.29    is_some (Thy_Info.lookup_theory name) orelse
    5.30 @@ -688,7 +692,7 @@
    5.31                timeit ("Document.update " ^ name) (fn () =>
    5.32                  Runtime.exn_trace_system (fn () =>
    5.33                    let
    5.34 -                    val ml_root = check_ml_root node;
    5.35 +                    val root_theory = check_root_theory node;
    5.36                      val keywords = the_default (Session.get_keywords ()) (get_keywords node);
    5.37                      val imports = map (apsnd Future.join) deps;
    5.38                      val imports_result_changed = exists (#4 o #1 o #2) imports;
    5.39 @@ -701,7 +705,7 @@
    5.40                          val node0 = node_of old_version name;
    5.41                          val init = init_theory imports node;
    5.42                          val proper_init =
    5.43 -                          is_some ml_root orelse
    5.44 +                          is_some root_theory orelse
    5.45                              check_theory false name node andalso
    5.46                              forall (fn (name, (_, node)) => check_theory true name node) imports;
    5.47  
    5.48 @@ -712,7 +716,7 @@
    5.49                          val common_command_exec =
    5.50                            (case common of
    5.51                              SOME id => (id, the_default Command.no_exec (the_entry node id))
    5.52 -                          | NONE => (Document_ID.none, Command.init_exec ml_root));
    5.53 +                          | NONE => (Document_ID.none, Command.init_exec root_theory));
    5.54  
    5.55                          val (updated_execs, (command_id', exec'), _) =
    5.56                            (print_execs, common_command_exec, if initial then SOME init else NONE)
     6.1 --- a/src/Pure/PIDE/resources.ML	Sat Dec 16 15:15:51 2017 +0100
     6.2 +++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 16:46:01 2017 +0100
     6.3 @@ -20,7 +20,8 @@
     6.4    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     6.5    val thy_path: Path.T -> Path.T
     6.6    val theory_qualifier: string -> string
     6.7 -  val import_name: string -> Path.T -> string -> {master_dir: Path.T, theory_name: string}
     6.8 +  val import_name: string -> Path.T -> string ->
     6.9 +    {node_name: Path.T, master_dir: Path.T, theory_name: string}
    6.10    val check_thy: Path.T -> string ->
    6.11     {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
    6.12      imports: (string * Position.T) list, keywords: Thy_Header.keywords}
    6.13 @@ -117,7 +118,8 @@
    6.14  
    6.15  fun import_name qualifier dir s =
    6.16    let val theory = theory_name qualifier (Thy_Header.import_name s) in
    6.17 -    if loaded_theory theory then {master_dir = Path.current, theory_name = theory}
    6.18 +    if loaded_theory theory
    6.19 +    then {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
    6.20      else
    6.21        let
    6.22          val node_name =
    6.23 @@ -127,7 +129,7 @@
    6.24                if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
    6.25                then Path.explode s
    6.26                else File.full_path dir (thy_path (Path.expand (Path.explode s))));
    6.27 -      in {master_dir = Path.dir node_name, theory_name = theory} end
    6.28 +      in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end
    6.29    end;
    6.30  
    6.31  fun check_file dir file = File.check_file (File.full_path dir file);
     7.1 --- a/src/Pure/PIDE/resources.scala	Sat Dec 16 15:15:51 2017 +0100
     7.2 +++ b/src/Pure/PIDE/resources.scala	Sat Dec 16 16:46:01 2017 +0100
     7.3 @@ -180,7 +180,8 @@
     7.4    def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
     7.5    {
     7.6      val imports =
     7.7 -      if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
     7.8 +      if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name))
     7.9 +      else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
    7.10        else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
    7.11        else Nil
    7.12      if (imports.isEmpty) None
     8.1 --- a/src/Pure/ROOT	Sat Dec 16 15:15:51 2017 +0100
     8.2 +++ b/src/Pure/ROOT	Sat Dec 16 16:46:01 2017 +0100
     8.3 @@ -8,3 +8,4 @@
     8.4    theories
     8.5      Pure (global)
     8.6      ML_Bootstrap (global)
     8.7 +    Sessions
     9.1 --- a/src/Pure/ROOT.ML	Sat Dec 16 15:15:51 2017 +0100
     9.2 +++ b/src/Pure/ROOT.ML	Sat Dec 16 16:46:01 2017 +0100
     9.3 @@ -290,6 +290,7 @@
     9.4  ML_file "PIDE/resources.ML";
     9.5  ML_file "Thy/present.ML";
     9.6  ML_file "Thy/thy_info.ML";
     9.7 +ML_file "Thy/sessions.ML";
     9.8  ML_file "PIDE/session.ML";
     9.9  ML_file "PIDE/protocol_message.ML";
    9.10  ML_file "PIDE/document.ML";
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Pure/Sessions.thy	Sat Dec 16 16:46:01 2017 +0100
    10.3 @@ -0,0 +1,19 @@
    10.4 +(*  Title:      Pure/Thy/Sessions.thy
    10.5 +    Author:     Makarius
    10.6 +
    10.7 +PIDE markup for session ROOT.
    10.8 +*)
    10.9 +
   10.10 +theory Sessions
   10.11 +  imports Pure
   10.12 +  keywords "session" :: thy_decl
   10.13 +    and "description" "options" "sessions" "theories" "document_files" :: quasi_command
   10.14 +    and "global"
   10.15 +begin
   10.16 +
   10.17 +ML \<open>
   10.18 +  Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT"
   10.19 +    Sessions.command_parser;
   10.20 +\<close>
   10.21 +
   10.22 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/Thy/sessions.ML	Sat Dec 16 16:46:01 2017 +0100
    11.3 @@ -0,0 +1,87 @@
    11.4 +(*  Title:      Pure/Thy/sessions.ML
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Support for session ROOT syntax.
    11.8 +*)
    11.9 +
   11.10 +signature SESSIONS =
   11.11 +sig
   11.12 +  val root_name: string
   11.13 +  val theory_name: string
   11.14 +  val command_parser: (Toplevel.transition -> Toplevel.transition) parser
   11.15 +end;
   11.16 +
   11.17 +structure Sessions: SESSIONS =
   11.18 +struct
   11.19 +
   11.20 +val root_name = "ROOT";
   11.21 +val theory_name = "Pure.Sessions";
   11.22 +
   11.23 +local
   11.24 +
   11.25 +val global =
   11.26 +  Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "global" -- Parse.$$$ ")") >> K true || Scan.succeed false;
   11.27 +
   11.28 +val theory_entry = Parse.position Parse.theory_name --| global;
   11.29 +
   11.30 +val theories =
   11.31 +  Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry);
   11.32 +
   11.33 +val document_files =
   11.34 +  Parse.$$$ "document_files" |--
   11.35 +    Parse.!!!
   11.36 +      (Scan.optional
   11.37 +        (Parse.$$$ "(" |--
   11.38 +            Parse.!!! (Parse.$$$ "in" |-- Parse.position Parse.path --| Parse.$$$ ")"))
   11.39 +        ("document", Position.none)
   11.40 +      -- Scan.repeat1 (Parse.position Parse.path));
   11.41 +
   11.42 +in
   11.43 +
   11.44 +val command_parser =
   11.45 +  Parse.session_name --
   11.46 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
   11.47 +  Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) --
   11.48 +  (Parse.$$$ "=" |-- Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
   11.49 +    Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
   11.50 +    Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
   11.51 +    Scan.optional (Parse.$$$ "sessions" |-- Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
   11.52 +    Scan.repeat theories --
   11.53 +    Scan.repeat document_files))
   11.54 +  >> (fn (((session, _), dir), ((((((_, descr), options), _), theories), document_files))) =>
   11.55 +    Toplevel.keep (fn state =>
   11.56 +      let
   11.57 +        val ctxt = Toplevel.context_of state;
   11.58 +        val thy = Toplevel.theory_of state;
   11.59 +        val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir;
   11.60 +
   11.61 +        val _ =
   11.62 +          Context_Position.report ctxt
   11.63 +            (Position.range_position (Symbol_Pos.range (Input.source_explode descr)))
   11.64 +            Markup.comment;
   11.65 +
   11.66 +        val _ =
   11.67 +          (options @ maps #1 theories) |> List.app (fn (x, y) =>
   11.68 +            ignore (Completion.check_option_value ctxt x y (Options.default ())));
   11.69 +
   11.70 +        val _ =
   11.71 +          maps #2 theories |> List.app (fn (s, pos) =>
   11.72 +            let
   11.73 +              val {node_name, theory_name, ...} =
   11.74 +                Resources.import_name session session_dir s
   11.75 +                  handle ERROR msg => error (msg ^ Position.here pos);
   11.76 +              val theory_path = the_default node_name (Resources.known_theory theory_name);
   11.77 +              val _ = Resources.check_file ctxt Path.current (Path.implode theory_path, pos);
   11.78 +            in () end);
   11.79 +
   11.80 +        val _ =
   11.81 +          document_files |> List.app (fn (doc_dir, doc_files) =>
   11.82 +            let
   11.83 +              val dir = Resources.check_dir ctxt session_dir doc_dir;
   11.84 +              val _ = List.app (ignore o Resources.check_file ctxt dir) doc_files;
   11.85 +            in () end);
   11.86 +      in () end));
   11.87 +
   11.88 +end;
   11.89 +
   11.90 +end;
    12.1 --- a/src/Pure/Thy/sessions.scala	Sat Dec 16 15:15:51 2017 +0100
    12.2 +++ b/src/Pure/Thy/sessions.scala	Sat Dec 16 16:46:01 2017 +0100
    12.3 @@ -19,6 +19,9 @@
    12.4  {
    12.5    /* base info and source dependencies */
    12.6  
    12.7 +  val root_name: String = "ROOT"
    12.8 +  val theory_name: String = "Pure.Sessions"
    12.9 +
   12.10    val DRAFT = "Draft"
   12.11  
   12.12    def is_pure(name: String): Boolean = name == Thy_Header.PURE
    13.1 --- a/src/Pure/Thy/thy_header.scala	Sat Dec 16 15:15:51 2017 +0100
    13.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Dec 16 16:46:01 2017 +0100
    13.3 @@ -76,7 +76,8 @@
    13.4    val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
    13.5    val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
    13.6  
    13.7 -  val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))
    13.8 +  val bootstrap_global_theories =
    13.9 +    (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE)
   13.10  
   13.11    private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
   13.12    private val File_Name = new Regex(""".*?([^/\\:]+)""")
   13.13 @@ -94,7 +95,8 @@
   13.14      s match {
   13.15        case Thy_File_Name(name) => bootstrap_name(name)
   13.16        case File_Name(name) =>
   13.17 -        ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
   13.18 +        if (name == Sessions.root_name) name
   13.19 +        else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
   13.20        case _ => ""
   13.21      }
   13.22  
    14.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Dec 16 15:15:51 2017 +0100
    14.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Dec 16 16:46:01 2017 +0100
    14.3 @@ -235,8 +235,9 @@
    14.4        }
    14.5      val nodes_status1 =
    14.6        (nodes_status /: iterator)({ case (status, (name, node)) =>
    14.7 -          if (!name.is_theory || PIDE.resources.session_base.loaded_theory(name) || node.is_empty)
    14.8 -            status
    14.9 +          if (!name.is_theory ||
   14.10 +              name.theory == Sessions.root_name ||
   14.11 +              PIDE.resources.session_base.loaded_theory(name) || node.is_empty) status
   14.12            else {
   14.13              val st = Protocol.node_status(snapshot.state, snapshot.version, name, node)
   14.14              status + (name -> st)