# HG changeset patch # User wenzelm # Date 1513439161 -3600 # Node ID 03d0c958d65a8d436ebcada6ad69e5dcd733359e # Parent 87038a574d098b7d7d2143ae8d79a7033c292384 PIDE markup for session ROOT files; diff -r 87038a574d09 -r 03d0c958d65a NEWS --- a/NEWS Sat Dec 16 15:15:51 2017 +0100 +++ b/NEWS Sat Dec 16 16:46:01 2017 +0100 @@ -44,6 +44,8 @@ *** Prover IDE -- Isabelle/Scala/jEdit *** +* PIDE markup for session ROOT files. + * Completion supports theory header imports, using theory base name. E.g. "Prob" may be completed to "HOL-Probability.Probability". diff -r 87038a574d09 -r 03d0c958d65a src/Doc/ROOT --- a/src/Doc/ROOT Sat Dec 16 15:15:51 2017 +0100 +++ b/src/Doc/ROOT Sat Dec 16 16:46:01 2017 +0100 @@ -148,7 +148,7 @@ Integration Isar Local_Theory - ML + "ML" Prelim Proof Syntax diff -r 87038a574d09 -r 03d0c958d65a src/HOL/ROOT --- a/src/HOL/ROOT Sat Dec 16 15:15:51 2017 +0100 +++ b/src/HOL/ROOT Sat Dec 16 16:46:01 2017 +0100 @@ -558,7 +558,7 @@ Lagrange List_to_Set_Comprehension_Examples LocaleTest2 - ML + "ML" MergeSort MonoidGroup Multiquote diff -r 87038a574d09 -r 03d0c958d65a src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Sat Dec 16 15:15:51 2017 +0100 +++ b/src/Pure/Isar/parse.ML Sat Dec 16 16:46:01 2017 +0100 @@ -67,6 +67,7 @@ val embedded: string parser val text: string parser val path: string parser + val session_name: string parser val theory_name: string parser val liberal_name: string parser val parname: string parser @@ -109,6 +110,9 @@ val thm_sel: Facts.interval list parser val thm: (Facts.ref * Token.src list) parser val thms1: (Facts.ref * Token.src list) list parser + val option_name: string parser + val option_value: string parser + val options: ((string * Position.T) * (string * Position.T)) list parser end; structure Parse: PARSE = @@ -272,6 +276,7 @@ val path = group (fn () => "file name/path specification") embedded; +val session_name = group (fn () => "session name") name; val theory_name = group (fn () => "theory name") name; val liberal_name = keyword_with Token.ident_or_symbolic || name; @@ -466,4 +471,16 @@ val thms1 = Scan.repeat1 thm; + +(* options *) + +val option_name = group (fn () => "option name") name; +val option_value = group (fn () => "option value") ((token real || token name) >> Token.content_of); + +val option = + position option_name :-- (fn (_, pos) => + Scan.optional ($$$ "=" |-- !!! (position option_value)) ("true", pos)); + +val options = $$$ "[" |-- list1 option --| $$$ "]"; + end; diff -r 87038a574d09 -r 03d0c958d65a src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Sat Dec 16 15:15:51 2017 +0100 +++ b/src/Pure/PIDE/document.ML Sat Dec 16 16:46:01 2017 +0100 @@ -578,14 +578,18 @@ val _ = Position.reports (map #2 parents_reports); in Resources.begin_theory master_dir header parents end; -fun check_ml_root node = - if member (op =) Thy_Header.ml_roots (#1 (#name (#header (get_header node)))) then - let - val master_dir = master_directory node; - val header = #header (get_header node); - val parent = Thy_Info.get_theory Thy_Header.ml_bootstrapN; - in SOME (Resources.begin_theory master_dir header [parent]) end - else NONE; +fun check_root_theory node = + let + val master_dir = master_directory node; + val header = #header (get_header node); + val header_name = #1 (#name header); + val parent = + if header_name = Sessions.root_name then + SOME (Thy_Info.get_theory Sessions.theory_name) + else if member (op =) Thy_Header.ml_roots header_name then + SOME (Thy_Info.get_theory Thy_Header.ml_bootstrapN) + else NONE; + in parent |> Option.map (fn thy => Resources.begin_theory master_dir header [thy]) end; fun check_theory full name node = is_some (Thy_Info.lookup_theory name) orelse @@ -688,7 +692,7 @@ timeit ("Document.update " ^ name) (fn () => Runtime.exn_trace_system (fn () => let - val ml_root = check_ml_root node; + val root_theory = check_root_theory node; val keywords = the_default (Session.get_keywords ()) (get_keywords node); val imports = map (apsnd Future.join) deps; val imports_result_changed = exists (#4 o #1 o #2) imports; @@ -701,7 +705,7 @@ val node0 = node_of old_version name; val init = init_theory imports node; val proper_init = - is_some ml_root orelse + is_some root_theory orelse check_theory false name node andalso forall (fn (name, (_, node)) => check_theory true name node) imports; @@ -712,7 +716,7 @@ val common_command_exec = (case common of SOME id => (id, the_default Command.no_exec (the_entry node id)) - | NONE => (Document_ID.none, Command.init_exec ml_root)); + | NONE => (Document_ID.none, Command.init_exec root_theory)); val (updated_execs, (command_id', exec'), _) = (print_execs, common_command_exec, if initial then SOME init else NONE) diff -r 87038a574d09 -r 03d0c958d65a src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Sat Dec 16 15:15:51 2017 +0100 +++ b/src/Pure/PIDE/resources.ML Sat Dec 16 16:46:01 2017 +0100 @@ -20,7 +20,8 @@ val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string - val import_name: string -> Path.T -> string -> {master_dir: Path.T, theory_name: string} + val import_name: string -> Path.T -> string -> + {node_name: Path.T, master_dir: Path.T, theory_name: string} val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} @@ -117,7 +118,8 @@ fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s) in - if loaded_theory theory then {master_dir = Path.current, theory_name = theory} + if loaded_theory theory + then {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory} else let val node_name = @@ -127,7 +129,7 @@ if Thy_Header.is_base_name s andalso Long_Name.is_qualified s then Path.explode s else File.full_path dir (thy_path (Path.expand (Path.explode s)))); - in {master_dir = Path.dir node_name, theory_name = theory} end + in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end end; fun check_file dir file = File.check_file (File.full_path dir file); diff -r 87038a574d09 -r 03d0c958d65a src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sat Dec 16 15:15:51 2017 +0100 +++ b/src/Pure/PIDE/resources.scala Sat Dec 16 16:46:01 2017 +0100 @@ -180,7 +180,8 @@ def special_header(name: Document.Node.Name): Option[Document.Node.Header] = { val imports = - if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP)) + if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name)) + else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP)) else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE)) else Nil if (imports.isEmpty) None diff -r 87038a574d09 -r 03d0c958d65a src/Pure/ROOT --- a/src/Pure/ROOT Sat Dec 16 15:15:51 2017 +0100 +++ b/src/Pure/ROOT Sat Dec 16 16:46:01 2017 +0100 @@ -8,3 +8,4 @@ theories Pure (global) ML_Bootstrap (global) + Sessions diff -r 87038a574d09 -r 03d0c958d65a src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Dec 16 15:15:51 2017 +0100 +++ b/src/Pure/ROOT.ML Sat Dec 16 16:46:01 2017 +0100 @@ -290,6 +290,7 @@ ML_file "PIDE/resources.ML"; ML_file "Thy/present.ML"; ML_file "Thy/thy_info.ML"; +ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; ML_file "PIDE/protocol_message.ML"; ML_file "PIDE/document.ML"; diff -r 87038a574d09 -r 03d0c958d65a src/Pure/Sessions.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Sessions.thy Sat Dec 16 16:46:01 2017 +0100 @@ -0,0 +1,19 @@ +(* Title: Pure/Thy/Sessions.thy + Author: Makarius + +PIDE markup for session ROOT. +*) + +theory Sessions + imports Pure + keywords "session" :: thy_decl + and "description" "options" "sessions" "theories" "document_files" :: quasi_command + and "global" +begin + +ML \ + Outer_Syntax.command \<^command_keyword>\session\ "PIDE markup for session ROOT" + Sessions.command_parser; +\ + +end diff -r 87038a574d09 -r 03d0c958d65a src/Pure/Thy/sessions.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/sessions.ML Sat Dec 16 16:46:01 2017 +0100 @@ -0,0 +1,87 @@ +(* Title: Pure/Thy/sessions.ML + Author: Makarius + +Support for session ROOT syntax. +*) + +signature SESSIONS = +sig + val root_name: string + val theory_name: string + val command_parser: (Toplevel.transition -> Toplevel.transition) parser +end; + +structure Sessions: SESSIONS = +struct + +val root_name = "ROOT"; +val theory_name = "Pure.Sessions"; + +local + +val global = + Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "global" -- Parse.$$$ ")") >> K true || Scan.succeed false; + +val theory_entry = Parse.position Parse.theory_name --| global; + +val theories = + Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry); + +val document_files = + Parse.$$$ "document_files" |-- + Parse.!!! + (Scan.optional + (Parse.$$$ "(" |-- + Parse.!!! (Parse.$$$ "in" |-- Parse.position Parse.path --| Parse.$$$ ")")) + ("document", Position.none) + -- Scan.repeat1 (Parse.position Parse.path)); + +in + +val command_parser = + Parse.session_name -- + Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] -- + Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) -- + (Parse.$$$ "=" |-- Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) -- + Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty -- + Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] -- + Scan.optional (Parse.$$$ "sessions" |-- Parse.!!! (Scan.repeat1 Parse.session_name)) [] -- + Scan.repeat theories -- + Scan.repeat document_files)) + >> (fn (((session, _), dir), ((((((_, descr), options), _), theories), document_files))) => + Toplevel.keep (fn state => + let + val ctxt = Toplevel.context_of state; + val thy = Toplevel.theory_of state; + val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir; + + val _ = + Context_Position.report ctxt + (Position.range_position (Symbol_Pos.range (Input.source_explode descr))) + Markup.comment; + + val _ = + (options @ maps #1 theories) |> List.app (fn (x, y) => + ignore (Completion.check_option_value ctxt x y (Options.default ()))); + + val _ = + maps #2 theories |> List.app (fn (s, pos) => + let + val {node_name, theory_name, ...} = + Resources.import_name session session_dir s + handle ERROR msg => error (msg ^ Position.here pos); + val theory_path = the_default node_name (Resources.known_theory theory_name); + val _ = Resources.check_file ctxt Path.current (Path.implode theory_path, pos); + in () end); + + val _ = + document_files |> List.app (fn (doc_dir, doc_files) => + let + val dir = Resources.check_dir ctxt session_dir doc_dir; + val _ = List.app (ignore o Resources.check_file ctxt dir) doc_files; + in () end); + in () end)); + +end; + +end; diff -r 87038a574d09 -r 03d0c958d65a src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sat Dec 16 15:15:51 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Sat Dec 16 16:46:01 2017 +0100 @@ -19,6 +19,9 @@ { /* base info and source dependencies */ + val root_name: String = "ROOT" + val theory_name: String = "Pure.Sessions" + val DRAFT = "Draft" def is_pure(name: String): Boolean = name == Thy_Header.PURE diff -r 87038a574d09 -r 03d0c958d65a src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sat Dec 16 15:15:51 2017 +0100 +++ b/src/Pure/Thy/thy_header.scala Sat Dec 16 16:46:01 2017 +0100 @@ -76,7 +76,8 @@ val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root") val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a)) - val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE)) + val bootstrap_global_theories = + (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE) private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""") private val File_Name = new Regex(""".*?([^/\\:]+)""") @@ -94,7 +95,8 @@ s match { case Thy_File_Name(name) => bootstrap_name(name) case File_Name(name) => - ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("") + if (name == Sessions.root_name) name + else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("") case _ => "" } diff -r 87038a574d09 -r 03d0c958d65a src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Sat Dec 16 15:15:51 2017 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Dec 16 16:46:01 2017 +0100 @@ -235,8 +235,9 @@ } val nodes_status1 = (nodes_status /: iterator)({ case (status, (name, node)) => - if (!name.is_theory || PIDE.resources.session_base.loaded_theory(name) || node.is_empty) - status + if (!name.is_theory || + name.theory == Sessions.root_name || + PIDE.resources.session_base.loaded_theory(name) || node.is_empty) status else { val st = Protocol.node_status(snapshot.state, snapshot.version, name, node) status + (name -> st)