# 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>\ROOTS_file\ "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>\generate_file\ "generate source file, with antiquotations" (Parse.path_binding -- (\<^keyword>\=\ |-- 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