# HG changeset patch
# User wenzelm
# Date 1607268457 -3600
# Node ID 2c26c283f3ee2c7d322689c3e6b084342ba7076d
# Parent  ec61e176768973ec925f1d8a63aabf555549e515
PIDE support for session ROOTS;

diff -r ec61e1767689 -r 2c26c283f3ee NEWS
--- a/NEWS	Sun Dec 06 16:14:16 2020 +0100
+++ b/NEWS	Sun Dec 06 16:27:37 2020 +0100
@@ -26,6 +26,8 @@
 collection and sharing of live data on the ML heap. It also includes
 information about the Java Runtime system.
 
+* PIDE support for session ROOTS: markup for directories.
+
 * Update to jedit-5.6.0, the latest release. This version works properly
 on macOS by default, without the special MacOSX plugin.
 
diff -r ec61e1767689 -r 2c26c283f3ee etc/settings
--- a/etc/settings	Sun Dec 06 16:14:16 2020 +0100
+++ b/etc/settings	Sun Dec 06 16:27:37 2020 +0100
@@ -25,6 +25,7 @@
 
 isabelle_scala_service 'isabelle.Scala_Functions'
 
+isabelle_scala_service 'isabelle.Sessions$File_Format'
 isabelle_scala_service 'isabelle.Bibtex$File_Format'
 
 isabelle_scala_service 'isabelle.ML_Statistics$Handler'
diff -r ec61e1767689 -r 2c26c283f3ee src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Dec 06 16:14:16 2020 +0100
+++ b/src/Pure/Pure.thy	Sun Dec 06 16:27:37 2020 +0100
@@ -20,7 +20,7 @@
     "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
   and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn
   and "axiomatization" :: thy_stmt
-  and "external_file" "bibtex_file" :: thy_load
+  and "external_file" "bibtex_file" "ROOTS_file" :: thy_load
   and "generate_file" :: thy_decl
   and "export_generated_files" :: diag
   and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix"
@@ -124,6 +124,25 @@
           in thy' end)));
 
   val _ =
+    Outer_Syntax.command \<^command_keyword>\<open>ROOTS_file\<close> "session ROOTS file"
+      (Resources.provide_parse_file >> (fn get_file =>
+        Toplevel.theory (fn thy =>
+          let
+            val ({src_path, lines, pos = pos0, ...}, thy') = get_file thy;
+            val ctxt = Proof_Context.init_global thy';
+            val dir = Path.dir (Path.expand (Resources.master_directory thy' + src_path));
+            val _ =
+              (lines, pos0) |-> fold (fn line => fn pos1 =>
+                let
+                  val pos2 = pos1 |> fold Position.advance (Symbol.explode line);
+                  val pos = Position.range_position (pos1, pos2);
+                  val _ =
+                    ignore (Resources.check_dir ctxt (SOME dir) (line, pos))
+                      handle ERROR msg => Output.error_message msg;
+                in pos2 |> Position.advance "\n" end);
+          in thy' end)));
+
+  val _ =
     Outer_Syntax.local_theory \<^command_keyword>\<open>generate_file\<close>
       "generate source file, with antiquotations"
       (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.embedded_input)
diff -r ec61e1767689 -r 2c26c283f3ee src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Dec 06 16:14:16 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Dec 06 16:27:37 2020 +0100
@@ -19,9 +19,10 @@
 {
   /* session and theory names */
 
+  val ROOTS: Path = Path.explode("ROOTS")
   val ROOT: Path = Path.explode("ROOT")
-  val ROOTS: Path = Path.explode("ROOTS")
 
+  val roots_name: String = "ROOTS"
   val root_name: String = "ROOT"
   val theory_name: String = "Pure.Sessions"
 
@@ -37,6 +38,21 @@
     name == root_name || name == "README" || name == "index" || name == "bib"
 
 
+  /* ROOTS file format */
+
+  class File_Format extends isabelle.File_Format
+  {
+    val format_name: String = roots_name
+    val file_ext = ""
+    override def detect(name: String): Boolean = name == roots_name
+
+    override def theory_suffix: String = "ROOTS_file"
+    override def theory_content(name: String): String =
+      """theory "ROOTS" imports Pure begin ROOTS_file """ +
+        Outer_Syntax.quote_string(name) + """ end"""
+  }
+
+
   /* base info and source dependencies */
 
   object Base