diff --git a/src/HOL/SPARK/Tools/spark.scala b/src/HOL/SPARK/Tools/spark.scala --- a/src/HOL/SPARK/Tools/spark.scala +++ b/src/HOL/SPARK/Tools/spark.scala @@ -1,23 +1,23 @@ /* Title: HOL/SPARK/Tools/spark.scala Author: Makarius Scala support for HOL-SPARK. */ package isabelle.spark import isabelle._ object SPARK { - class Load_Command1 extends Command_Span.Load_Command("spark_vcg") + class Load_Command1 extends Command_Span.Load_Command("spark_vcg", Scala_Project.here) { override val extensions: List[String] = List("vcg", "fdl", "rls") } - class Load_Command2 extends Command_Span.Load_Command("spark_siv") + class Load_Command2 extends Command_Span.Load_Command("spark_siv", Scala_Project.here) { override val extensions: List[String] = List("siv", "fdl", "rls") } } diff --git a/src/Pure/Isar/keyword.ML b/src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML +++ b/src/Pure/Isar/keyword.ML @@ -1,292 +1,296 @@ (* Title: Pure/Isar/keyword.ML Author: Makarius Isar keyword classification. *) signature KEYWORD = sig val diag: string val document_heading: string val document_body: string val document_raw: string val thy_begin: string val thy_end: string val thy_decl: string val thy_decl_block: string val thy_defn: string val thy_stmt: string val thy_load: string val thy_goal: string val thy_goal_defn: string val thy_goal_stmt: string val qed: string val qed_script: string val qed_block: string val qed_global: string val prf_goal: string val prf_block: string val next_block: string val prf_open: string val prf_close: string val prf_chain: string val prf_decl: string val prf_asm: string val prf_asm_goal: string val prf_script: string val prf_script_goal: string val prf_script_asm_goal: string val before_command: string val quasi_command: string - type spec = string * string list + type spec = {kind: string, load_command: string * Position.T, tags: string list} + val command_spec: string * string list -> spec val no_spec: spec val before_command_spec: spec val quasi_command_spec: spec val document_heading_spec: spec val document_body_spec: spec type keywords val minor_keywords: keywords -> Scan.lexicon val major_keywords: keywords -> Scan.lexicon val empty_keywords: keywords val merge_keywords: keywords * keywords -> keywords val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords val add_minor_keywords: string list -> keywords -> keywords val add_major_keywords: string list -> keywords -> keywords val no_major_keywords: keywords -> keywords val is_keyword: keywords -> string -> bool val is_command: keywords -> string -> bool val is_literal: keywords -> string -> bool val dest_commands: keywords -> string list val command_markup: keywords -> string -> Markup.T option val command_kind: keywords -> string -> string option val command_tags: keywords -> string -> string list val is_vacuous: keywords -> string -> bool val is_diag: keywords -> string -> bool val is_document_heading: keywords -> string -> bool val is_document_body: keywords -> string -> bool val is_document_raw: keywords -> string -> bool val is_document: keywords -> string -> bool val is_theory_end: keywords -> string -> bool val is_theory_load: keywords -> string -> bool val is_theory: keywords -> string -> bool val is_theory_body: keywords -> string -> bool val is_proof: keywords -> string -> bool val is_proof_body: keywords -> string -> bool val is_theory_goal: keywords -> string -> bool val is_proof_goal: keywords -> string -> bool val is_qed: keywords -> string -> bool val is_qed_global: keywords -> string -> bool val is_proof_open: keywords -> string -> bool val is_proof_close: keywords -> string -> bool val is_proof_asm: keywords -> string -> bool val is_improper: keywords -> string -> bool val is_printed: keywords -> string -> bool end; structure Keyword: KEYWORD = struct (** keyword classification **) (* kinds *) val diag = "diag"; val document_heading = "document_heading"; val document_body = "document_body"; val document_raw = "document_raw"; val thy_begin = "thy_begin"; val thy_end = "thy_end"; val thy_decl = "thy_decl"; val thy_decl_block = "thy_decl_block"; val thy_defn = "thy_defn"; val thy_stmt = "thy_stmt"; val thy_load = "thy_load"; val thy_goal = "thy_goal"; val thy_goal_defn = "thy_goal_defn"; val thy_goal_stmt = "thy_goal_stmt"; val qed = "qed"; val qed_script = "qed_script"; val qed_block = "qed_block"; val qed_global = "qed_global"; val prf_goal = "prf_goal"; val prf_block = "prf_block"; val next_block = "next_block"; val prf_open = "prf_open"; val prf_close = "prf_close"; val prf_chain = "prf_chain"; val prf_decl = "prf_decl"; val prf_asm = "prf_asm"; val prf_asm_goal = "prf_asm_goal"; val prf_script = "prf_script"; val prf_script_goal = "prf_script_goal"; val prf_script_asm_goal = "prf_script_asm_goal"; val before_command = "before_command"; val quasi_command = "quasi_command"; val command_kinds = [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; (* specifications *) -type spec = string * string list; +type spec = {kind: string, load_command: string * Position.T, tags: string list}; -val no_spec: spec = ("", []); -val before_command_spec: spec = (before_command, []); -val quasi_command_spec: spec = (quasi_command, []); -val document_heading_spec: spec = ("document_heading", ["document"]); -val document_body_spec: spec = ("document_body", ["document"]); +fun command_spec (kind, tags) : spec = + {kind = kind, load_command = ("", Position.none), tags = tags}; + +val no_spec = command_spec ("", []); +val before_command_spec = command_spec (before_command, []); +val quasi_command_spec = command_spec (quasi_command, []); +val document_heading_spec = command_spec ("document_heading", ["document"]); +val document_body_spec = command_spec ("document_body", ["document"]); type entry = {pos: Position.T, id: serial, kind: string, tags: string list}; -fun check_spec pos (kind, tags) : entry = +fun check_spec pos ({kind, tags, ...}: spec) : entry = if not (member (op =) command_kinds kind) then error ("Unknown outer syntax keyword kind " ^ quote kind) else {pos = pos, id = serial (), kind = kind, tags = tags}; (** keyword tables **) (* type keywords *) datatype keywords = Keywords of {minor: Scan.lexicon, major: Scan.lexicon, commands: entry Symtab.table}; fun minor_keywords (Keywords {minor, ...}) = minor; fun major_keywords (Keywords {major, ...}) = major; fun make_keywords (minor, major, commands) = Keywords {minor = minor, major = major, commands = commands}; fun map_keywords f (Keywords {minor, major, commands}) = make_keywords (f (minor, major, commands)); (* build keywords *) val empty_keywords = make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty); fun merge_keywords (Keywords {minor = minor1, major = major1, commands = commands1}, Keywords {minor = minor2, major = major2, commands = commands2}) = make_keywords (Scan.merge_lexicons (minor1, minor2), Scan.merge_lexicons (major1, major2), Symtab.merge (K true) (commands1, commands2)); val add_keywords = - fold (fn ((name, pos), spec as (kind, _)) => map_keywords (fn (minor, major, commands) => + fold (fn ((name, pos), spec as {kind, ...}: spec) => map_keywords (fn (minor, major, commands) => if kind = "" orelse kind = before_command orelse kind = quasi_command then let val minor' = Scan.extend_lexicon (Symbol.explode name) minor; in (minor', major, commands) end else let val entry = check_spec pos spec; val major' = Scan.extend_lexicon (Symbol.explode name) major; val commands' = Symtab.update (name, entry) commands; in (minor, major', commands') end)); val add_minor_keywords = add_keywords o map (fn name => ((name, Position.none), no_spec)); val add_major_keywords = - add_keywords o map (fn name => ((name, Position.none), (diag, []))); + add_keywords o map (fn name => ((name, Position.none), command_spec (diag, []))); val no_major_keywords = map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); (* keyword status *) fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s); fun is_command (Keywords {commands, ...}) = Symtab.defined commands; fun is_literal keywords = is_keyword keywords orf is_command keywords; fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands; (* command keywords *) fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands; fun command_markup keywords name = lookup_command keywords name |> Option.map (fn {pos, id, ...} => Position.make_entity_markup {def = false} id Markup.command_keywordN (name, pos)); fun command_kind keywords = Option.map #kind o lookup_command keywords; fun command_tags keywords name = (case lookup_command keywords name of SOME {tags, ...} => tags | NONE => []); (* command categories *) fun command_category ks = let val tab = Symtab.make_set ks; fun pred keywords name = (case lookup_command keywords name of NONE => false | SOME {kind, ...} => Symtab.defined tab kind); in pred end; val is_vacuous = command_category [diag, document_heading, document_body, document_raw]; val is_diag = command_category [diag]; val is_document_heading = command_category [document_heading]; val is_document_body = command_category [document_body]; val is_document_raw = command_category [document_raw]; val is_document = command_category [document_heading, document_body, document_raw]; val is_theory_end = command_category [thy_end]; val is_theory_load = command_category [thy_load]; val is_theory = command_category [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt]; val is_theory_body = command_category [thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt]; val is_proof = command_category [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; val is_proof_body = command_category [diag, document_heading, document_body, document_raw, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; val is_theory_goal = command_category [thy_goal, thy_goal_defn, thy_goal_stmt]; val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal]; val is_qed = command_category [qed, qed_script, qed_block]; val is_qed_global = command_category [qed_global]; val is_proof_open = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open]; val is_proof_close = command_category [qed, qed_script, qed_block, prf_close]; val is_proof_asm = command_category [prf_asm, prf_asm_goal]; val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal]; fun is_printed keywords = is_theory_goal keywords orf is_proof keywords; end; diff --git a/src/Pure/PIDE/command_span.scala b/src/Pure/PIDE/command_span.scala --- a/src/Pure/PIDE/command_span.scala +++ b/src/Pure/PIDE/command_span.scala @@ -1,146 +1,151 @@ /* Title: Pure/PIDE/command_span.scala Author: Makarius Syntactic representation of command spans. */ package isabelle import scala.collection.mutable import scala.util.parsing.input.CharSequenceReader object Command_Span { /* loaded files */ object Loaded_Files { val none: Loaded_Files = Loaded_Files(Nil, -1) } sealed case class Loaded_Files(files: List[String], index: Int) - class Load_Command(val name: String) extends Isabelle_System.Service + abstract class Load_Command(val name: String, val here: Scala_Project.Here) + extends Isabelle_System.Service { override def toString: String = name + def position: Position.T = here.position + def extensions: List[String] = Nil def loaded_files(tokens: List[(Token, Int)]): Loaded_Files = tokens.collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) match { case Some((file, i)) => extensions match { case Nil => Loaded_Files(List(file), i) case exts => Loaded_Files(exts.map(ext => file + "." + ext), i) } case None => Loaded_Files.none } } + object Load_Command_Default extends Load_Command("", Scala_Project.here) + lazy val load_commands: List[Load_Command] = - new Load_Command("") :: Isabelle_System.make_services(classOf[Load_Command]) + Load_Command_Default :: Isabelle_System.make_services(classOf[Load_Command]) /* span kind */ sealed abstract class Kind { override def toString: String = this match { case Command_Span(name, _) => proper_string(name) getOrElse "" case Ignored_Span => "" case Malformed_Span => "" case Theory_Span => "" } } case class Command_Span(name: String, pos: Position.T) extends Kind case object Ignored_Span extends Kind case object Malformed_Span extends Kind case object Theory_Span extends Kind /* span */ sealed case class Span(kind: Kind, content: List[Token]) { def is_theory: Boolean = kind == Theory_Span def name: String = kind match { case k: Command_Span => k.name case _ => "" } def position: Position.T = kind match { case k: Command_Span => k.pos case _ => Position.none } def keyword_pos(start: Token.Pos): Token.Pos = kind match { case _: Command_Span => content.iterator.takeWhile(tok => !tok.is_command).foldLeft(start)(_.advance(_)) case _ => start } def is_kind(keywords: Keyword.Keywords, pred: String => Boolean, other: Boolean): Boolean = keywords.kinds.get(name) match { case Some(k) => pred(k) case None => other } def is_begin: Boolean = content.exists(_.is_begin) def is_end: Boolean = content.exists(_.is_end) def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content)) def length: Int = content.foldLeft(0)(_ + _.source.length) def compact_source: (String, Span) = { val source = Token.implode(content) val content1 = new mutable.ListBuffer[Token] var i = 0 for (Token(kind, s) <- content) { val n = s.length val s1 = source.substring(i, i + n) content1 += Token(kind, s1) i += n } (source, Span(kind, content1.toList)) } def clean_arguments: List[(Token, Int)] = { if (name.nonEmpty) { def clean(toks: List[(Token, Int)]): List[(Token, Int)] = toks match { case (t1, i1) :: (t2, i2) :: rest => if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest) else (t1, i1) :: clean((t2, i2) :: rest) case _ => toks } clean(content.zipWithIndex.filter({ case (t, _) => t.is_proper })) .dropWhile({ case (t, _) => !t.is_command }) .dropWhile({ case (t, _) => t.is_command }) } else Nil } def is_load_command(syntax: Outer_Syntax): Boolean = syntax.load_command(name).isDefined def loaded_files(syntax: Outer_Syntax): Loaded_Files = syntax.load_command(name) match { case None => Loaded_Files.none case Some(a) => load_commands.find(_.name == a) match { case Some(load_command) => load_command.loaded_files(clean_arguments) case None => error("Undefined load command function: " + a) } } } val empty: Span = Span(Ignored_Span, Nil) def unparsed(source: String, theory: Boolean): Span = { val kind = if (theory) Theory_Span else Malformed_Span Span(kind, List(Token(Token.Kind.UNPARSED, source))) } } diff --git a/src/Pure/PIDE/markup.ML b/src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML +++ b/src/Pure/PIDE/markup.ML @@ -1,834 +1,836 @@ (* Title: Pure/PIDE/markup.ML Author: Makarius Quasi-abstract markup elements. *) signature MARKUP = sig type T = string * Properties.T val empty: T val is_empty: T -> bool val properties: Properties.T -> T -> T val nameN: string val name: string -> T -> T val xnameN: string val xname: string -> T -> T val kindN: string val serialN: string val serial_properties: int -> Properties.T val instanceN: string val meta_titleN: string val meta_title: T val meta_creatorN: string val meta_creator: T val meta_contributorN: string val meta_contributor: T val meta_dateN: string val meta_date: T val meta_licenseN: string val meta_license: T val meta_descriptionN: string val meta_description: T val languageN: string val symbolsN: string val delimitedN: string val is_delimited: Properties.T -> bool val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T val language_Isar: bool -> T val language_method: T val language_attribute: T val language_sort: bool -> T val language_type: bool -> T val language_term: bool -> T val language_prop: bool -> T val language_ML: bool -> T val language_SML: bool -> T val language_document: bool -> T val language_document_marker: T val language_antiquotation: T val language_text: bool -> T val language_verbatim: bool -> T val language_latex: bool -> T val language_rail: T val language_path: bool -> T val language_url: bool -> T val language_mixfix: T val bindingN: string val binding: T val entityN: string val entity: string -> string -> T val defN: string val refN: string val completionN: string val completion: T val no_completionN: string val no_completion: T val updateN: string val update: T val lineN: string val end_lineN: string val offsetN: string val end_offsetN: string val fileN: string val idN: string val positionN: string val position: T val position_properties: string list val position_property: Properties.entry -> bool val def_name: string -> string val def_theoryN: string val expressionN: string val expression: string -> T val citationN: string val citation: string -> T val pathN: string val path: string -> T val export_pathN: string val export_path: string -> T val urlN: string val url: string -> T val docN: string val doc: string -> T val toolN: string val tool: string -> T val markupN: string val consistentN: string val unbreakableN: string val block_properties: string list val indentN: string val widthN: string val blockN: string val block: bool -> int -> T val breakN: string val break: int -> int -> T val fbreakN: string val fbreak: T val itemN: string val item: T val wordsN: string val words: T val hiddenN: string val hidden: T val deleteN: string val delete: T + val load_commandN: string val bash_functionN: string val scala_functionN: string val system_optionN: string val sessionN: string val theoryN: string val classN: string val localeN: string val bundleN: string val type_nameN: string val constantN: string val axiomN: string val factN: string val oracleN: string val fixedN: string val fixed: string -> T val caseN: string val case_: string -> T val dynamic_factN: string val dynamic_fact: string -> T val literal_factN: string val literal_fact: string -> T val attributeN: string val methodN: string val method_modifierN: string val tfreeN: string val tfree: T val tvarN: string val tvar: T val freeN: string val free: T val skolemN: string val skolem: T val boundN: string val bound: T val varN: string val var: T val numeralN: string val numeral: T val literalN: string val literal: T val delimiterN: string val delimiter: T val inner_stringN: string val inner_string: T val inner_cartoucheN: string val inner_cartouche: T val token_rangeN: string val token_range: T val sortingN: string val sorting: T val typingN: string val typing: T val class_parameterN: string val class_parameter: T val ML_keyword1N: string val ML_keyword1: T val ML_keyword2N: string val ML_keyword2: T val ML_keyword3N: string val ML_keyword3: T val ML_delimiterN: string val ML_delimiter: T val ML_tvarN: string val ML_tvar: T val ML_numeralN: string val ML_numeral: T val ML_charN: string val ML_char: T val ML_stringN: string val ML_string: T val ML_commentN: string val ML_comment: T val ML_defN: string val ML_openN: string val ML_structureN: string val ML_typingN: string val ML_typing: T val ML_breakpointN: string val ML_breakpoint: int -> T val antiquotedN: string val antiquoted: T val antiquoteN: string val antiquote: T val file_typeN: string val antiquotationN: string val ML_antiquotationN: string val document_antiquotationN: string val document_antiquotation_optionN: string val raw_textN: string val raw_text: T val plain_textN: string val plain_text: T val paragraphN: string val paragraph: T val text_foldN: string val text_fold: T val document_markerN: string val document_marker: T val document_tagN: string val document_tag: string -> T val document_latexN: string val document_latex: T val markdown_paragraphN: string val markdown_paragraph: T val markdown_itemN: string val markdown_item: T val markdown_bulletN: string val markdown_bullet: int -> T val markdown_listN: string val markdown_list: string -> T val itemizeN: string val enumerateN: string val descriptionN: string val inputN: string val input: bool -> Properties.T -> T val command_keywordN: string val command_keyword: T val commandN: string val command_properties: T -> T val keywordN: string val keyword_properties: T -> T val stringN: string val string: T val alt_stringN: string val alt_string: T val verbatimN: string val verbatim: T val cartoucheN: string val cartouche: T val commentN: string val comment: T val keyword1N: string val keyword1: T val keyword2N: string val keyword2: T val keyword3N: string val keyword3: T val quasi_keywordN: string val quasi_keyword: T val improperN: string val improper: T val operatorN: string val operator: T val comment1N: string val comment1: T val comment2N: string val comment2: T val comment3N: string val comment3: T val elapsedN: string val cpuN: string val gcN: string val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T val parse_command_timing_properties: Properties.T -> ({file: string, offset: int, name: string} * Time.time) option val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T val command_indentN: string val command_indent: int -> T val goalN: string val goal: T val subgoalN: string val subgoal: string -> T val taskN: string val forkedN: string val forked: T val joinedN: string val joined: T val runningN: string val running: T val finishedN: string val finished: T val failedN: string val failed: T val canceledN: string val canceled: T val initializedN: string val initialized: T val finalizedN: string val finalized: T val consolidatingN: string val consolidating: T val consolidatedN: string val consolidated: T val exec_idN: string val initN: string val statusN: string val status: T val resultN: string val result: T val writelnN: string val writeln: T val stateN: string val state: T val informationN: string val information: T val tracingN: string val tracing: T val warningN: string val warning: T val legacyN: string val legacy: T val errorN: string val error: T val systemN: string val system: T val protocolN: string val reportN: string val report: T val no_reportN: string val no_report: T val badN: string val bad: unit -> T val intensifyN: string val intensify: T val countN: string val ML_profiling_entryN: string val ML_profiling_entry: {name: string, count: int} -> T val ML_profilingN: string val ML_profiling: string -> T val browserN: string val graphviewN: string val theory_exportsN: string val sendbackN: string val paddingN: string val padding_line: Properties.entry val padding_command: Properties.entry val dialogN: string val dialog: serial -> string -> T val jedit_actionN: string val functionN: string val ML_statistics: {pid: int, stats_dir: string} -> Properties.T val commands_accepted: Properties.T val assign_update: Properties.T val removed_versions: Properties.T val invoke_scala: string -> string -> Properties.T val cancel_scala: string -> Properties.T val task_statistics: Properties.entry val command_timing: Properties.entry val theory_timing: Properties.entry val session_timing: Properties.entry val loading_theory: string -> Properties.T val build_session_finished: Properties.T val print_operationsN: string val print_operations: Properties.T val exportN: string type export_args = {id: string option, serial: serial, theory_name: string, name: string, executable: bool, compress: bool, strict: bool} val export: export_args -> Properties.T val debugger_state: string -> Properties.T val debugger_output: string -> Properties.T val simp_trace_panelN: string val simp_trace_logN: string val simp_trace_stepN: string val simp_trace_recurseN: string val simp_trace_hintN: string val simp_trace_ignoreN: string val simp_trace_cancel: serial -> Properties.T type output = Output.output * Output.output val no_output: output val add_mode: string -> (T -> output) -> unit val output: T -> output val enclose: T -> Output.output -> Output.output val markup: T -> string -> string val markups: T list -> string -> string val markup_only: T -> string val markup_report: string -> string end; structure Markup: MARKUP = struct (** markup elements **) (* basic markup *) type T = string * Properties.T; val empty = ("", []); fun is_empty ("", _) = true | is_empty _ = false; fun properties more_props ((elem, props): T) = (elem, fold_rev Properties.put more_props props); fun markup_elem name = (name, (name, []): T); fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T); fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T); (* misc properties *) val nameN = "name"; fun name a = properties [(nameN, a)]; val xnameN = "xname"; fun xname a = properties [(xnameN, a)]; val kindN = "kind"; val serialN = "serial"; fun serial_properties i = [(serialN, Value.print_int i)]; val instanceN = "instance"; (* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *) val (meta_titleN, meta_title) = markup_elem "meta_title"; val (meta_creatorN, meta_creator) = markup_elem "meta_creator"; val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor"; val (meta_dateN, meta_date) = markup_elem "meta_date"; val (meta_licenseN, meta_license) = markup_elem "meta_license"; val (meta_descriptionN, meta_description) = markup_elem "meta_description"; (* embedded languages *) val languageN = "language"; val symbolsN = "symbols"; val antiquotesN = "antiquotes"; val delimitedN = "delimited" fun is_delimited props = Properties.get props delimitedN = SOME "true"; fun language {name, symbols, antiquotes, delimited} = (languageN, [(nameN, name), (symbolsN, Value.print_bool symbols), (antiquotesN, Value.print_bool antiquotes), (delimitedN, Value.print_bool delimited)]); fun language' {name, symbols, antiquotes} delimited = language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited}; val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false}; val language_method = language {name = "method", symbols = true, antiquotes = false, delimited = false}; val language_attribute = language {name = "attribute", symbols = true, antiquotes = false, delimited = false}; val language_sort = language' {name = "sort", symbols = true, antiquotes = false}; val language_type = language' {name = "type", symbols = true, antiquotes = false}; val language_term = language' {name = "term", symbols = true, antiquotes = false}; val language_prop = language' {name = "prop", symbols = true, antiquotes = false}; val language_ML = language' {name = "ML", symbols = false, antiquotes = true}; val language_SML = language' {name = "SML", symbols = false, antiquotes = false}; val language_document = language' {name = "document", symbols = false, antiquotes = true}; val language_document_marker = language {name = "document_marker", symbols = true, antiquotes = true, delimited = true}; val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; val language_text = language' {name = "text", symbols = true, antiquotes = false}; val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false}; val language_latex = language' {name = "latex", symbols = false, antiquotes = false}; val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true}; val language_path = language' {name = "path", symbols = false, antiquotes = false}; val language_url = language' {name = "url", symbols = false, antiquotes = false}; val language_mixfix = language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true}; (* formal entities *) val (bindingN, binding) = markup_elem "binding"; val entityN = "entity"; fun entity kind name = (entityN, (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)])); val defN = "def"; val refN = "ref"; (* completion *) val (completionN, completion) = markup_elem "completion"; val (no_completionN, no_completion) = markup_elem "no_completion"; val (updateN, update) = markup_elem "update"; (* position *) val lineN = "line"; val end_lineN = "end_line"; val offsetN = "offset"; val end_offsetN = "end_offset"; val fileN = "file"; val idN = "id"; val (positionN, position) = markup_elem "position"; val position_properties = [lineN, offsetN, end_offsetN, fileN, idN]; fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry); (* position "def" names *) fun make_def a = "def_" ^ a; val def_names = Symtab.make (map (fn a => (a, make_def a)) position_properties); fun def_name a = (case Symtab.lookup def_names a of SOME b => b | NONE => make_def a); val def_theoryN = "def_theory"; (* expression *) val expressionN = "expression"; fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]); (* citation *) val (citationN, citation) = markup_string "citation" nameN; (* external resources *) val (pathN, path) = markup_string "path" nameN; val (export_pathN, export_path) = markup_string "export_path" nameN; val (urlN, url) = markup_string "url" nameN; val (docN, doc) = markup_string "doc" nameN; val (toolN, tool) = markup_string "tool" nameN; (* pretty printing *) val markupN = "markup"; val consistentN = "consistent"; val unbreakableN = "unbreakable"; val indentN = "indent"; val block_properties = [markupN, consistentN, unbreakableN, indentN]; val widthN = "width"; val blockN = "block"; fun block c i = (blockN, (if c then [(consistentN, Value.print_bool c)] else []) @ (if i <> 0 then [(indentN, Value.print_int i)] else [])); val breakN = "break"; fun break w i = (breakN, (if w <> 0 then [(widthN, Value.print_int w)] else []) @ (if i <> 0 then [(indentN, Value.print_int i)] else [])); val (fbreakN, fbreak) = markup_elem "fbreak"; val (itemN, item) = markup_elem "item"; (* text properties *) val (wordsN, words) = markup_elem "words"; val (hiddenN, hidden) = markup_elem "hidden"; val (deleteN, delete) = markup_elem "delete"; (* misc entities *) +val load_commandN = "load_command"; val bash_functionN = "bash_function"; val scala_functionN = "scala_function"; val system_optionN = "system_option"; val sessionN = "session"; val theoryN = "theory"; val classN = "class"; val localeN = "locale"; val bundleN = "bundle"; val type_nameN = "type_name"; val constantN = "constant"; val axiomN = "axiom"; val factN = "fact"; val oracleN = "oracle"; val (fixedN, fixed) = markup_string "fixed" nameN; val (caseN, case_) = markup_string "case" nameN; val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; val (literal_factN, literal_fact) = markup_string "literal_fact" nameN; val attributeN = "attribute"; val methodN = "method"; val method_modifierN = "method_modifier"; (* inner syntax *) val (tfreeN, tfree) = markup_elem "tfree"; val (tvarN, tvar) = markup_elem "tvar"; val (freeN, free) = markup_elem "free"; val (skolemN, skolem) = markup_elem "skolem"; val (boundN, bound) = markup_elem "bound"; val (varN, var) = markup_elem "var"; val (numeralN, numeral) = markup_elem "numeral"; val (literalN, literal) = markup_elem "literal"; val (delimiterN, delimiter) = markup_elem "delimiter"; val (inner_stringN, inner_string) = markup_elem "inner_string"; val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"; val (token_rangeN, token_range) = markup_elem "token_range"; val (sortingN, sorting) = markup_elem "sorting"; val (typingN, typing) = markup_elem "typing"; val (class_parameterN, class_parameter) = markup_elem "class_parameter"; (* ML *) val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1"; val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2"; val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3"; val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter"; val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar"; val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral"; val (ML_charN, ML_char) = markup_elem "ML_char"; val (ML_stringN, ML_string) = markup_elem "ML_string"; val (ML_commentN, ML_comment) = markup_elem "ML_comment"; val ML_defN = "ML_def"; val ML_openN = "ML_open"; val ML_structureN = "ML_structure"; val (ML_typingN, ML_typing) = markup_elem "ML_typing"; val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN; (* antiquotations *) val (antiquotedN, antiquoted) = markup_elem "antiquoted"; val (antiquoteN, antiquote) = markup_elem "antiquote"; val file_typeN = "file_type"; val antiquotationN = "antiquotation"; val ML_antiquotationN = "ML_antiquotation"; val document_antiquotationN = "document_antiquotation"; val document_antiquotation_optionN = "document_antiquotation_option"; (* document text *) val (raw_textN, raw_text) = markup_elem "raw_text"; val (plain_textN, plain_text) = markup_elem "plain_text"; val (paragraphN, paragraph) = markup_elem "paragraph"; val (text_foldN, text_fold) = markup_elem "text_fold"; val (document_markerN, document_marker) = markup_elem "document_marker"; val (document_tagN, document_tag) = markup_string "document_tag" nameN; val (document_latexN, document_latex) = markup_elem "document_latex"; (* Markdown document structure *) val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph"; val (markdown_itemN, markdown_item) = markup_elem "markdown_item"; val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth"; val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN; val itemizeN = "itemize"; val enumerateN = "enumerate"; val descriptionN = "description"; (* formal input *) val inputN = "input"; fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props); (* outer syntax *) val (command_keywordN, command_keyword) = markup_elem "command_keyword"; val commandN = "command"; val command_properties = properties [(kindN, commandN)]; val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)]; val (keyword1N, keyword1) = markup_elem "keyword1"; val (keyword2N, keyword2) = markup_elem "keyword2"; val (keyword3N, keyword3) = markup_elem "keyword3"; val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword"; val (improperN, improper) = markup_elem "improper"; val (operatorN, operator) = markup_elem "operator"; val (stringN, string) = markup_elem "string"; val (alt_stringN, alt_string) = markup_elem "alt_string"; val (verbatimN, verbatim) = markup_elem "verbatim"; val (cartoucheN, cartouche) = markup_elem "cartouche"; val (commentN, comment) = markup_elem "comment"; (* comments *) val (comment1N, comment1) = markup_elem "comment1"; val (comment2N, comment2) = markup_elem "comment2"; val (comment3N, comment3) = markup_elem "comment3"; (* timing *) val elapsedN = "elapsed"; val cpuN = "cpu"; val gcN = "gc"; fun timing_properties {elapsed, cpu, gc} = [(elapsedN, Value.print_time elapsed), (cpuN, Value.print_time cpu), (gcN, Value.print_time gc)]; val timingN = "timing"; fun timing t = (timingN, timing_properties t); (* command timing *) fun parse_command_timing_properties props = (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of (SOME file, SOME offset, SOME name) => SOME ({file = file, offset = Value.parse_int offset, name = name}, Properties.seconds props elapsedN) | _ => NONE); (* indentation *) val (command_indentN, command_indent) = markup_int "command_indent" indentN; (* goals *) val (goalN, goal) = markup_elem "goal"; val (subgoalN, subgoal) = markup_string "subgoal" nameN; (* command status *) val taskN = "task"; val (forkedN, forked) = markup_elem "forked"; val (joinedN, joined) = markup_elem "joined"; val (runningN, running) = markup_elem "running"; val (finishedN, finished) = markup_elem "finished"; val (failedN, failed) = markup_elem "failed"; val (canceledN, canceled) = markup_elem "canceled"; val (initializedN, initialized) = markup_elem "initialized"; val (finalizedN, finalized) = markup_elem "finalized"; val (consolidatingN, consolidating) = markup_elem "consolidating"; val (consolidatedN, consolidated) = markup_elem "consolidated"; (* messages *) val exec_idN = "exec_id"; val initN = "init"; val (statusN, status) = markup_elem "status"; val (resultN, result) = markup_elem "result"; val (writelnN, writeln) = markup_elem "writeln"; val (stateN, state) = markup_elem "state" val (informationN, information) = markup_elem "information"; val (tracingN, tracing) = markup_elem "tracing"; val (warningN, warning) = markup_elem "warning"; val (legacyN, legacy) = markup_elem "legacy"; val (errorN, error) = markup_elem "error"; val (systemN, system) = markup_elem "system"; val protocolN = "protocol"; val (reportN, report) = markup_elem "report"; val (no_reportN, no_report) = markup_elem "no_report"; val badN = "bad"; fun bad () = (badN, serial_properties (serial ())); val (intensifyN, intensify) = markup_elem "intensify"; (* ML profiling *) val countN = "count"; val ML_profiling_entryN = "ML_profiling_entry"; fun ML_profiling_entry {name, count} = (ML_profiling_entryN, [(nameN, name), (countN, Value.print_int count)]); val (ML_profilingN, ML_profiling) = markup_string "ML_profiling" kindN; (* active areas *) val browserN = "browser" val graphviewN = "graphview"; val theory_exportsN = "theory_exports"; val sendbackN = "sendback"; val paddingN = "padding"; val padding_line = (paddingN, "line"); val padding_command = (paddingN, "command"); val dialogN = "dialog"; fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]); val jedit_actionN = "jedit_action"; (* protocol message functions *) val functionN = "function" fun ML_statistics {pid, stats_dir} = [(functionN, "ML_statistics"), ("pid", Value.print_int pid), ("stats_dir", stats_dir)]; val commands_accepted = [(functionN, "commands_accepted")]; val assign_update = [(functionN, "assign_update")]; val removed_versions = [(functionN, "removed_versions")]; fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; val task_statistics = (functionN, "task_statistics"); val command_timing = (functionN, "command_timing"); val theory_timing = (functionN, "theory_timing"); val session_timing = (functionN, "session_timing"); fun loading_theory name = [("function", "loading_theory"), (nameN, name)]; val build_session_finished = [("function", "build_session_finished")]; val print_operationsN = "print_operations"; val print_operations = [(functionN, print_operationsN)]; (* export *) val exportN = "export"; type export_args = {id: string option, serial: serial, theory_name: string, name: string, executable: bool, compress: bool, strict: bool}; fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) = [(functionN, exportN), (idN, the_default "" id), (serialN, Value.print_int serial), ("theory_name", theory_name), (nameN, name), ("executable", Value.print_bool executable), ("compress", Value.print_bool compress), ("strict", Value.print_bool strict)]; (* debugger *) fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)]; fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)]; (* simplifier trace *) val simp_trace_panelN = "simp_trace_panel"; val simp_trace_logN = "simp_trace_log"; val simp_trace_stepN = "simp_trace_step"; val simp_trace_recurseN = "simp_trace_recurse"; val simp_trace_hintN = "simp_trace_hint"; val simp_trace_ignoreN = "simp_trace_ignore"; fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)]; (** print mode operations **) type output = Output.output * Output.output; val no_output = ("", ""); local val default = {output = Output_Primitives.markup_fn}; val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]); in fun add_mode name output = Synchronized.change modes (fn tab => (if not (Symtab.defined tab name) then () else Output.warning ("Redefining markup mode " ^ quote name); Symtab.update (name, {output = output}) tab)); fun get_mode () = the_default default (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); end; fun output m = if is_empty m then no_output else #output (get_mode ()) m; val enclose = output #-> Library.enclose; fun markup m = let val (bg, en) = output m in Library.enclose (Output.escape bg) (Output.escape en) end; val markups = fold_rev markup; fun markup_only m = markup m ""; fun markup_report "" = "" | markup_report txt = markup report txt; end; diff --git a/src/Pure/PIDE/protocol.ML b/src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML +++ b/src/Pure/PIDE/protocol.ML @@ -1,177 +1,178 @@ (* Title: Pure/PIDE/protocol.ML Author: Makarius Protocol message formats for interactive proof documents. *) structure Protocol: sig end = struct val _ = Protocol_Command.define "Prover.echo" (fn args => List.app writeln args); val _ = Protocol_Command.define "Prover.stop" (fn rc :: msgs => (List.app Output.system_message msgs; raise Protocol_Command.STOP (Value.parse_int rc))); val _ = Protocol_Command.define "Prover.options" (fn [options_yxml] => (Options.set_default (Options.decode (YXML.parse_body options_yxml)); Isabelle_Process.init_options_interactive ())); val _ = Protocol_Command.define "Prover.init_session" (fn [yxml] => Resources.init_session_yxml yxml); val _ = Protocol_Command.define "Document.define_blob" (fn [digest, content] => Document.change_state (Document.define_blob digest content)); fun decode_command id name parents_xml blobs_xml toks_xml sources : Document.command = let open XML.Decode; val parents = list string parents_xml; val (blobs_digests, blobs_index) = blobs_xml |> let val message = YXML.string_of_body o Protocol_Message.command_positions id; val blob = triple string string (option string) #> (fn (a, b, c) => {file_node = a, src_path = Path.explode b, digest = c}); in pair (list (variant [fn ([], a) => Exn.Res (blob a), fn ([], a) => Exn.Exn (ERROR (message a))])) int end; val toks = list (pair int int) toks_xml; in {command_id = Document_ID.parse id, name = name, parents = parents, blobs_digests = blobs_digests, blobs_index = blobs_index, tokens = toks ~~ sources} end; fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [[XML.Text (space_implode "," ids)]]; val _ = Protocol_Command.define "Document.define_command" (fn id :: name :: parents :: blobs :: toks :: sources => let val command = decode_command id name (YXML.parse_body parents) (YXML.parse_body blobs) (YXML.parse_body toks) sources; val _ = Document.change_state (Document.define_command command); in commands_accepted [id] end); val _ = Protocol_Command.define "Document.define_commands" (fn args => let fun decode arg = let open XML.Decode; val (id, (name, (parents_xml, (blobs_xml, (toks_xml, sources))))) = pair string (pair string (pair I (pair I (pair I (list string))))) (YXML.parse_body arg); in decode_command id name parents_xml blobs_xml toks_xml sources end; val commands = map decode args; val _ = Document.change_state (fold Document.define_command commands); in commands_accepted (map (Value.print_int o #command_id) commands) end); val _ = Protocol_Command.define "Document.discontinue_execution" (fn [] => Execution.discontinue ()); val _ = Protocol_Command.define "Document.cancel_exec" (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); val _ = Protocol_Command.define "Document.update" (Future.task_context "Document.update" (Future.new_group NONE) (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml => Document.change_state (fn state => let val old_id = Document_ID.parse old_id_string; val new_id = Document_ID.parse new_id_string; val consolidate = YXML.parse_body consolidate_yxml |> let open XML.Decode in list string end; val edits = edits_yxml |> map (YXML.parse_body #> let open XML.Decode in pair string (variant [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => let val (master, (name, (imports, (keywords, errors)))) = pair string (pair string (pair (list string) (pair (list (pair string (pair string (list string)))) (list YXML.string_of_body)))) a; val imports' = map (rpair Position.none) imports; - val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; + val keywords' = + map (fn (x, y) => ((x, Position.none), Keyword.command_spec y)) keywords; val header = Thy_Header.make (name, Position.none) imports' keywords'; in Document.Deps {master = master, header = header, errors = errors} end, fn (a :: b, c) => Document.Perspective (bool_atom a, map int_atom b, list (pair int (pair string (list string))) c)]) end); val _ = Execution.discontinue (); val (edited, removed, assign_update, state') = Document.update old_id new_id edits consolidate state; val _ = (singleton o Future.forks) {name = "Document.update/remove", group = NONE, deps = Execution.snapshot removed, pri = Task_Queue.urgent_pri + 2, interrupts = false} (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); val _ = Output.protocol_message Markup.assign_update [(new_id, edited, assign_update) |> let open XML.Encode; fun encode_upd (a, bs) = string (space_implode "," (map Value.print_int (a :: bs))); in triple int (list string) (list encode_upd) end]; in Document.start_execution state' end))); val _ = Protocol_Command.define "Document.remove_versions" (fn [versions_yxml] => Document.change_state (fn state => let val versions = YXML.parse_body versions_yxml |> let open XML.Decode in list int end; val state1 = Document.remove_versions versions state; val _ = Output.protocol_message Markup.removed_versions [[XML.Text (versions_yxml)]]; in state1 end)); val _ = Protocol_Command.define "Document.dialog_result" (fn [serial, result] => Active.dialog_result (Value.parse_int serial) result handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn); val _ = Protocol_Command.define "ML_Heap.full_gc" (fn [] => ML_Heap.full_gc ()); val _ = Protocol_Command.define "ML_Heap.share_common_data" (fn [] => ML_Heap.share_common_data ()); end; diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,440 +1,454 @@ (* Title: Pure/PIDE/resources.ML Author: Makarius Resources for theories and auxiliary files. *) signature RESOURCES = sig val default_qualifier: string val init_session: {session_positions: (string * Properties.T) list, session_directories: (string * string) list, session_chapters: (string * string) list, bibtex_entries: (string * string list) list, command_timings: Properties.T list, + load_commands: (string * Position.T) list, scala_functions: (string * (bool * Position.T)) list, global_theories: (string * string) list, loaded_theories: string list} -> unit val init_session_yxml: string -> unit val init_session_file: Path.T -> unit val finish_session_base: unit -> unit val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string val session_chapter: string -> string val last_timing: Toplevel.transition -> Time.time + val check_load_command: Proof.context -> string * Position.T -> string val scala_functions: unit -> string list val check_scala_function: Proof.context -> string * Position.T -> string * bool val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string val theory_bibtex_entries: string -> string list val find_theory_file: string -> Path.T option 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} val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser val parse_file: (theory -> Token.file) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser val provide_parse_file: (theory -> Token.file * theory) parser val loaded_files_current: theory -> bool val check_path: Proof.context -> Path.T option -> Input.source -> Path.T val check_file: Proof.context -> Path.T option -> Input.source -> Path.T val check_dir: Proof.context -> Path.T option -> Input.source -> Path.T val check_session_dir: Proof.context -> Path.T option -> Input.source -> Path.T end; structure Resources: RESOURCES = struct (* command timings *) type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty; fun update_timings props = (case Markup.parse_command_timing_properties props of SOME ({file, offset, name}, time) => Symtab.map_default (file, Inttab.empty) (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) | NONE => I); fun make_timings command_timings = fold update_timings command_timings empty_timings; fun approximative_id name pos = (case (Position.file_of pos, Position.offset_of pos) of (SOME file, SOME offset) => if name = "" then NONE else SOME {file = file, offset = offset, name = name} | _ => NONE); fun get_timings timings tr = (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of SOME {file, offset, name} => (case Symtab.lookup timings file of SOME offsets => (case Inttab.lookup offsets offset of SOME (name', time) => if name = name' then SOME time else NONE | NONE => NONE) | NONE => NONE) | NONE => NONE) |> the_default Time.zeroTime; (* session base *) val default_qualifier = "Draft"; type entry = {pos: Position.T, serial: serial}; fun make_entry props : entry = {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = ({session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, session_chapters = Symtab.empty: string Symtab.table, bibtex_entries = Symtab.empty: string list Symtab.table, timings = empty_timings, + load_commands = []: (string * Position.T) list, scala_functions = Symtab.empty: (bool * Position.T) Symtab.table}, {global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}); val global_session_base = Synchronized.var "Sessions.base" empty_session_base; fun init_session {session_positions, session_directories, session_chapters, bibtex_entries, - command_timings, scala_functions, global_theories, loaded_theories} = + command_timings, load_commands, scala_functions, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => ({session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = Symtab.build (session_directories |> fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))), session_chapters = Symtab.make session_chapters, bibtex_entries = Symtab.make bibtex_entries, timings = make_timings command_timings, + load_commands = load_commands, scala_functions = Symtab.make scala_functions}, {global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories})); fun init_session_yxml yxml = let val (session_positions, (session_directories, (session_chapters, (bibtex_entries, - (command_timings, (scala_functions, (global_theories, loaded_theories))))))) = + (command_timings, (load_commands, (scala_functions, (global_theories, loaded_theories)))))))) = YXML.parse_body yxml |> let open XML.Decode in (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list (pair string string)) (pair (list (pair string (list string))) (pair (list properties) - (pair (list (pair string (pair bool properties))) - (pair (list (pair string string)) (list string)))))))) + (pair (list (pair string properties)) + (pair (list (pair string (pair bool properties))) + (pair (list (pair string string)) (list string))))))))) end; in init_session {session_positions = session_positions, session_directories = session_directories, session_chapters = session_chapters, bibtex_entries = bibtex_entries, command_timings = command_timings, + load_commands = (map o apsnd) Position.of_properties load_commands, scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions, global_theories = global_theories, loaded_theories = loaded_theories} end; fun init_session_file path = init_session_yxml (File.read path) before File.rm path; fun finish_session_base () = Synchronized.change global_session_base (apfst (K (#1 empty_session_base))); fun get_session_base f = f (Synchronized.value global_session_base); fun get_session_base1 f = get_session_base (f o #1); fun get_session_base2 f = get_session_base (f o #2); fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a; fun check_session ctxt arg = Completion.check_item "session" (fn (name, {pos, serial}) => Position.make_entity_markup {def = false} serial Markup.sessionN (name, pos)) (get_session_base1 #session_positions) ctxt arg; fun session_chapter name = the_default "Unsorted" (Symtab.lookup (get_session_base1 #session_chapters) name); fun last_timing tr = get_timings (get_session_base1 #timings) tr; +fun check_load_command ctxt arg = + Completion.check_entity Markup.load_commandN (get_session_base1 #load_commands) ctxt arg; + (* Scala functions *) (*raw bootstrap environment*) fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); (*regular resources*) fun scala_function a = (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a)); fun check_scala_function ctxt arg = let val funs = scala_functions () |> sort_strings |> map scala_function; val name = Completion.check_entity Markup.scala_functionN (map (apsnd #2) funs) ctxt arg; val multi = (case AList.lookup (op =) funs name of SOME (multi, _) => multi | NONE => false); in (name, multi) end; val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\scala_function\ (Scan.lift Parse.embedded_position) (#1 oo check_scala_function) #> ML_Antiquotation.inline_embedded \<^binding>\scala_function\ (Args.context -- Scan.lift Parse.embedded_position >> (uncurry check_scala_function #> #1 #> ML_Syntax.print_string)) #> ML_Antiquotation.value_embedded \<^binding>\scala\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) => let val (name, multi) = check_scala_function ctxt arg; val func = if multi then "Scala.function" else "Scala.function1"; in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end))); (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) = let val provided' = Library.merge (op =) (provided1, provided2) in make_files (master_dir, imports, provided') end ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun begin_theory master_dir {name, imports, keywords} parents = - Theory.begin_theory name parents - |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, [])) - |> Thy_Header.add_keywords keywords; + let + val thy = + Theory.begin_theory name parents + |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, [])) + |> Thy_Header.add_keywords keywords; + val ctxt = Proof_Context.init_global thy; + val _ = List.app (ignore o check_load_command ctxt o #load_command o #2) keywords; + in thy end; (* theory files *) val thy_path = Path.ext "thy"; fun theory_qualifier theory = (case global_theory theory of SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); fun theory_name qualifier theory = if Long_Name.is_qualified theory orelse is_some (global_theory theory) then theory else Long_Name.qualify qualifier theory; fun theory_bibtex_entries theory = Symtab.lookup_list (get_session_base1 #bibtex_entries) (theory_qualifier theory); fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); val session = theory_qualifier thy_name; val dirs = Symtab.lookup_list (get_session_base1 #session_directories) session; in dirs |> get_first (fn dir => let val path = dir + thy_file in if File.is_file path then SOME path else NONE end) end; fun make_theory_node node_name theory = {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; fun loaded_theory_node theory = {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s); fun theory_node () = make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory; in if not (Thy_Header.is_base_name s) then theory_node () else if loaded_theory theory then loaded_theory_node theory else (case find_theory_file theory of SOME node_name => make_theory_node node_name theory | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ()) end; fun check_file dir file = File.check_file (File.full_path dir file); fun check_thy dir thy_name = let val thy_base_name = Long_Name.base_name thy_name; val master_file = (case find_theory_file thy_name of SOME path => check_file Path.current path | NONE => check_file dir (thy_path (Path.basic thy_base_name))); val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* load files *) fun parse_files make_paths = Scan.ahead Parse.not_eof -- Parse.path_input >> (fn (tok, source) => fn thy => (case Token.get_files tok of [] => let val master_dir = master_directory thy; val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val src_paths = make_paths (Path.explode name); in map (Command.read_file master_dir pos delimited) src_paths end | files => map Exn.release files)); val parse_file = parse_files single >> (fn f => f #> the_single); fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); fun provide_parse_files make_paths = parse_files make_paths >> (fn files => fn thy => let val fs = files thy; val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; in (fs, thy') end); val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single); fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun loaded_files_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* formal check *) fun formal_check check_file ctxt opt_dir source = let val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val _ = Context_Position.report ctxt pos (Markup.language_path delimited); fun err msg = error (msg ^ Position.here pos); val dir = (case opt_dir of SOME dir => dir | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = dir + Path.explode name handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); val _ : Path.T = check_file path handle ERROR msg => err msg; in path end; val check_path = formal_check I; val check_file = formal_check File.check_file; val check_dir = formal_check File.check_dir; fun check_session_dir ctxt opt_dir s = let val dir = Path.expand (check_dir ctxt opt_dir s); val ok = File.is_file (dir + Path.explode("ROOT")) orelse File.is_file (dir + Path.explode("ROOTS")); in if ok then dir else error ("Bad session root directory (missing ROOT or ROOTS): " ^ Path.print dir ^ Position.here (Input.pos_of s)) end; (* antiquotations *) local fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => (check ctxt NONE source; Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)) |> Latex.enclose_text "\\isatt{" "}")); fun ML_antiq check = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => check ctxt (SOME Path.current) source |> ML_Syntax.print_path); in val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> Document_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> Document_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> Document_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> ML_Antiquotation.value_embedded \<^binding>\path_binding\ (Scan.lift (Parse.position Parse.path) >> (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); end; end; diff --git a/src/Pure/PIDE/resources.scala b/src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala +++ b/src/Pure/PIDE/resources.scala @@ -1,451 +1,453 @@ /* Title: Pure/PIDE/resources.scala Author: Makarius Resources for theories and auxiliary files. */ package isabelle import scala.util.parsing.input.Reader import java.io.{File => JFile} object Resources { def empty: Resources = new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap) } class Resources( val sessions_structure: Sessions.Structure, val session_base: Sessions.Base, val log: Logger = No_Logger, command_timings: List[Properties.T] = Nil) { resources => /* init session */ def init_session_yxml: String = { import XML.Encode._ YXML.string_of_body( pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(pair(string, string)), pair(list(pair(string, list(string))), pair(list(properties), + pair(list(pair(string, properties)), pair(list(pair(string, pair(bool, properties))), - pair(list(pair(string, string)), list(string))))))))( + pair(list(pair(string, string)), list(string)))))))))( (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (sessions_structure.session_chapters, (sessions_structure.bibtex_entries, (command_timings, + (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)), (Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))), (session_base.global_theories.toList, - session_base.loaded_theories.keys))))))))) + session_base.loaded_theories.keys)))))))))) } /* file formats */ def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] = File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name)) def make_theory_content(thy_name: Document.Node.Name): Option[String] = File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) def is_hidden(name: Document.Node.Name): Boolean = !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot)) /* file-system operations */ def append(dir: String, source_path: Path): String = (Path.explode(dir) + source_path).expand.implode def append(node_name: Document.Node.Name, source_path: Path): String = append(node_name.master_dir, source_path) def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = { val node = append(dir, file) val master_dir = append(dir, file.dir) Document.Node.Name(node, master_dir, theory) } def loaded_theory_node(theory: String): Document.Node.Name = Document.Node.Name(theory, "", theory) /* source files of Isabelle/ML bootstrap */ def source_file(raw_name: String): Option[String] = { if (Path.is_wellformed(raw_name)) { if (Path.is_valid(raw_name)) { def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None val path = Path.explode(raw_name) val path1 = if (path.is_absolute || path.is_current) check(path) else { check(Path.explode("~~/src/Pure") + path) orElse (if (Isabelle_System.getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path)) } Some(File.platform_path(path1 getOrElse path)) } else None } else Some(raw_name) } /* theory files */ def load_commands(syntax: Outer_Syntax, name: Document.Node.Name) : () => List[Command_Span.Span] = { val (is_utf8, raw_text) = with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString)) () => { if (syntax.has_load_commands(raw_text)) { val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text)) syntax.parse_spans(text).filter(_.is_load_command(syntax)) } else Nil } } def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name, spans: List[Command_Span.Span]) : List[Path] = { val dir = name.master_dir_path for { span <- spans; file <- span.loaded_files(syntax).files } yield (dir + Path.explode(file)).expand } def pure_files(syntax: Outer_Syntax): List[Path] = { val pure_dir = Path.explode("~~/src/Pure") for { (name, theory) <- Thy_Header.ml_roots path = (pure_dir + Path.explode(name)).expand node_name = Document.Node.Name(path.implode, path.dir.implode, theory) file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)()) } yield file } def theory_name(qualifier: String, theory: String): String = if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory)) theory else Long_Name.qualify(qualifier, theory) def find_theory_node(theory: String): Option[Document.Node.Name] = { val thy_file = Path.basic(Long_Name.base_name(theory)).thy val session = session_base.theory_qualifier(theory) val dirs = sessions_structure.get(session) match { case Some(info) => info.dirs case None => Nil } dirs.collectFirst({ case dir if (dir + thy_file).is_file => file_node(dir + thy_file, theory = theory) }) } def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = { val theory = theory_name(qualifier, Thy_Header.import_name(s)) def theory_node = file_node(Path.explode(s).thy, dir = dir, theory = theory) if (!Thy_Header.is_base_name(s)) theory_node else if (session_base.loaded_theory(theory)) loaded_theory_node(theory) else { find_theory_node(theory) match { case Some(node_name) => node_name case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node } } } def import_name(name: Document.Node.Name, s: String): Document.Node.Name = import_name(session_base.theory_qualifier(name), name.master_dir, s) def import_name(info: Sessions.Info, s: String): Document.Node.Name = import_name(info.name, info.dir.implode, s) def find_theory(file: JFile): Option[Document.Node.Name] = { for { qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile) theory_base <- proper_string(Thy_Header.theory_name(file.getName)) theory = theory_name(qualifier, theory_base) theory_node <- find_theory_node(theory) if File.eq(theory_node.path.file, file) } yield theory_node } def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = { val context_session = session_base.theory_qualifier(context_name) val context_dir = try { Some(context_name.master_dir_path) } catch { case ERROR(_) => None } (for { (session, (info, _)) <- sessions_structure.imports_graph.iterator dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator theory <- Thy_Header.try_read_dir(dir).iterator if Completion.completed(s)(theory) } yield { if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory else Long_Name.qualify(session, theory) }).toList.sorted } def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { val path = name.path if (path.is_file) using(Scan.byte_reader(path.file))(f) else if (name.node == name.theory) error("Cannot load theory " + quote(name.theory)) else error ("Cannot load theory file " + path) } def check_thy(node_name: Document.Node.Name, reader: Reader[Char], command: Boolean = true, strict: Boolean = true): Document.Node.Header = { if (node_name.is_theory && reader.source.length > 0) { try { val header = Thy_Header.read(node_name, reader, command = command, strict = strict) val imports = header.imports.map({ case (s, pos) => val name = import_name(node_name, s) if (Sessions.exclude_theory(name.theory_base_name)) error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos)) (name, pos) }) Document.Node.Header(imports, header.keywords, header.abbrevs) } catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } } else Document.Node.no_header } /* special header */ def special_header(name: Document.Node.Name): Option[Document.Node.Header] = { val imports = 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 else Some(Document.Node.Header(imports.map((_, Position.none)))) } /* blobs */ def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] = (for { (node_name, node) <- nodes.iterator if !session_base.loaded_theory(node_name) cmd <- node.load_commands.iterator name <- cmd.blobs_undefined.iterator } yield name).toList /* document changes */ def parse_change( reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text], consolidate: List[Document.Node.Name]): Session.Change = Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate) def commit(change: Session.Change): Unit = {} /* theory and file dependencies */ def dependencies( thys: List[(Document.Node.Name, Position.T)], progress: Progress = new Progress): Dependencies[Unit] = Dependencies.empty[Unit].require_thys((), thys, progress = progress) def session_dependencies(info: Sessions.Info, progress: Progress = new Progress) : Dependencies[Options] = { info.theories.foldLeft(Dependencies.empty[Options]) { case (dependencies, (options, thys)) => dependencies.require_thys(options, for { (thy, pos) <- thys } yield (import_name(info, thy), pos), progress = progress) } } object Dependencies { def empty[A]: Dependencies[A] = new Dependencies[A](Nil, Map.empty) private def show_path(names: List[Document.Node.Name]): String = names.map(name => quote(name.theory)).mkString(" via ") private def cycle_msg(names: List[Document.Node.Name]): String = "Cyclic dependency of " + show_path(names) private def required_by(initiators: List[Document.Node.Name]): String = if (initiators.isEmpty) "" else "\n(required by " + show_path(initiators.reverse) + ")" } final class Dependencies[A] private( rev_entries: List[Document.Node.Entry], seen: Map[Document.Node.Name, A]) { private def cons(entry: Document.Node.Entry): Dependencies[A] = new Dependencies[A](entry :: rev_entries, seen) def require_thy(adjunct: A, thy: (Document.Node.Name, Position.T), initiators: List[Document.Node.Name] = Nil, progress: Progress = new Progress): Dependencies[A] = { val (name, pos) = thy def message: String = "The error(s) above occurred for theory " + quote(name.theory) + Dependencies.required_by(initiators) + Position.here(pos) if (seen.isDefinedAt(name)) this else { val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct)) if (session_base.loaded_theory(name)) dependencies1 else { try { if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators)) progress.expose_interrupt() val header = try { with_thy_reader(name, check_thy(name, _, command = false)).cat_errors(message) } catch { case ERROR(msg) => cat_error(msg, message) } val entry = Document.Node.Entry(name, header) dependencies1.require_thys(adjunct, header.imports_pos, initiators = name :: initiators, progress = progress).cons(entry) } catch { case e: Throwable => dependencies1.cons(Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e)))) } } } } def require_thys(adjunct: A, thys: List[(Document.Node.Name, Position.T)], progress: Progress = new Progress, initiators: List[Document.Node.Name] = Nil): Dependencies[A] = thys.foldLeft(this)(_.require_thy(adjunct, _, progress = progress, initiators = initiators)) def entries: List[Document.Node.Entry] = rev_entries.reverse def theories: List[Document.Node.Name] = entries.map(_.name) def theories_adjunct: List[(Document.Node.Name, A)] = theories.map(name => (name, seen(name))) def errors: List[String] = entries.flatMap(_.header.errors) def check_errors: Dependencies[A] = errors match { case Nil => this case errs => error(cat_lines(errs)) } lazy val theory_graph: Document.Node.Name.Graph[Unit] = { val regular = theories.toSet val irregular = (for { entry <- entries.iterator imp <- entry.header.imports if !regular(imp) } yield imp).toSet Document.Node.Name.make_graph( irregular.toList.map(name => ((name, ()), Nil)) ::: entries.map(entry => ((entry.name, ()), entry.header.imports))) } lazy val loaded_theories: Graph[String, Outer_Syntax] = entries.foldLeft(session_base.loaded_theories) { case (graph, entry) => val name = entry.name.theory val imports = entry.header.imports.map(_.theory) val graph1 = (name :: imports).foldLeft(graph)(_.default_node(_, Outer_Syntax.empty)) val graph2 = imports.foldLeft(graph1)(_.add_edge(_, name)) val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node) val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header graph2.map_node(name, _ => syntax) } def get_syntax(name: Document.Node.Name): Outer_Syntax = loaded_theories.get_node(name.theory) def load_commands: List[(Document.Node.Name, List[Command_Span.Span])] = theories.zip( Par_List.map((e: () => List[Command_Span.Span]) => e(), theories.map(name => resources.load_commands(get_syntax(name), name)))) .filter(p => p._2.nonEmpty) def loaded_files(name: Document.Node.Name, spans: List[Command_Span.Span]) : (String, List[Path]) = { val theory = name.theory val syntax = get_syntax(name) val files1 = resources.loaded_files(syntax, name, spans) val files2 = if (theory == Thy_Header.PURE) pure_files(syntax) else Nil (theory, files1 ::: files2) } def loaded_files: List[Path] = for { (name, spans) <- load_commands file <- loaded_files(name, spans)._2 } yield file def imported_files: List[Path] = { val base_theories = loaded_theories.all_preds(theories.map(_.theory)). filter(session_base.loaded_theories.defined) base_theories.map(theory => session_base.known_theories(theory).name.path) ::: base_theories.flatMap(session_base.known_loaded_files.withDefaultValue(Nil)) } lazy val overall_syntax: Outer_Syntax = Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node)) override def toString: String = entries.toString } } diff --git a/src/Pure/Thy/thy_header.ML b/src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML +++ b/src/Pure/Thy/thy_header.ML @@ -1,211 +1,213 @@ (* Title: Pure/Thy/thy_header.ML Author: Makarius Static theory header information. *) signature THY_HEADER = sig type keywords = ((string * Position.T) * Keyword.spec) list type header = {name: string * Position.T, imports: (string * Position.T) list, keywords: keywords} val make: string * Position.T -> (string * Position.T) list -> keywords -> header val theoryN: string val bootstrap_keywords: Keyword.keywords val add_keywords: keywords -> theory -> theory val get_keywords: theory -> Keyword.keywords val get_keywords': Proof.context -> Keyword.keywords val ml_bootstrapN: string val ml_roots: string list val bootstrap_thys: string list val is_base_name: string -> bool val import_name: string -> string val args: header parser val read_tokens: Position.T -> Token.T list -> header val read: Position.T -> string -> header end; structure Thy_Header: THY_HEADER = struct (** keyword declarations **) (* header *) type keywords = ((string * Position.T) * Keyword.spec) list; type header = {name: string * Position.T, imports: (string * Position.T) list, keywords: keywords}; fun make name imports keywords : header = {name = name, imports = imports, keywords = keywords}; (* bootstrap keywords *) val chapterN = "chapter"; val sectionN = "section"; val subsectionN = "subsection"; val subsubsectionN = "subsubsection"; val paragraphN = "paragraph"; val subparagraphN = "subparagraph"; val textN = "text"; val txtN = "txt"; val text_rawN = "text_raw"; val theoryN = "theory"; val importsN = "imports"; val keywordsN = "keywords"; val abbrevsN = "abbrevs"; val beginN = "begin"; val bootstrap_keywords = Keyword.empty_keywords |> Keyword.add_keywords [(("%", \<^here>), Keyword.no_spec), (("(", \<^here>), Keyword.no_spec), ((")", \<^here>), Keyword.no_spec), ((",", \<^here>), Keyword.no_spec), (("::", \<^here>), Keyword.no_spec), (("=", \<^here>), Keyword.no_spec), (("and", \<^here>), Keyword.no_spec), ((beginN, \<^here>), Keyword.quasi_command_spec), ((importsN, \<^here>), Keyword.quasi_command_spec), ((keywordsN, \<^here>), Keyword.quasi_command_spec), ((abbrevsN, \<^here>), Keyword.quasi_command_spec), ((chapterN, \<^here>), Keyword.document_heading_spec), ((sectionN, \<^here>), Keyword.document_heading_spec), ((subsectionN, \<^here>), Keyword.document_heading_spec), ((subsubsectionN, \<^here>), Keyword.document_heading_spec), ((paragraphN, \<^here>), Keyword.document_heading_spec), ((subparagraphN, \<^here>), Keyword.document_heading_spec), ((textN, \<^here>), Keyword.document_body_spec), ((txtN, \<^here>), Keyword.document_body_spec), - ((text_rawN, \<^here>), (Keyword.document_raw, ["document"])), - ((theoryN, \<^here>), (Keyword.thy_begin, ["theory"])), - (("ML", \<^here>), (Keyword.thy_decl, ["ML"]))]; + ((text_rawN, \<^here>), Keyword.command_spec (Keyword.document_raw, ["document"])), + ((theoryN, \<^here>), Keyword.command_spec (Keyword.thy_begin, ["theory"])), + (("ML", \<^here>), Keyword.command_spec (Keyword.thy_decl, ["ML"]))]; (* theory data *) structure Data = Theory_Data ( type T = Keyword.keywords; val empty = bootstrap_keywords; val merge = Keyword.merge_keywords; ); val add_keywords = Data.map o Keyword.add_keywords; val get_keywords = Data.get; val get_keywords' = get_keywords o Proof_Context.theory_of; (** concrete syntax **) (* names *) val ml_bootstrapN = "ML_Bootstrap"; val ml_roots = ["ML_Root0", "ML_Root"]; val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"]; fun is_base_name s = s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s) fun import_name s = if String.isSuffix ".thy" s then error ("Malformed theory import: " ^ quote s) else Path.file_name (Path.explode s); (* header args *) local fun imports name = if name = Context.PureN then Scan.succeed [] else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 Parse.theory_name); val load_command = - Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; + Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.position Parse.name) --| Parse.$$$ ")") + ("", Position.none); val keyword_spec = Parse.group (fn () => "outer syntax keyword specification") - ((Parse.name --| load_command) -- Document_Source.old_tags); + ((Parse.name -- load_command) -- Document_Source.old_tags) >> + (fn ((a, b), c) => {kind = a, load_command = b, tags = c}); val keyword_decl = Scan.repeat1 Parse.string_position -- Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec >> (fn (names, spec) => map (rpair spec) names); val abbrevs = Parse.and_list1 (Scan.repeat1 Parse.text -- (Parse.$$$ "=" |-- Parse.!!! (Scan.repeat1 Parse.text)) >> uncurry (map_product pair)) >> flat; val keyword_decls = Parse.and_list1 keyword_decl >> flat; in val args = Parse.theory_name :|-- (fn (name, pos) => imports name -- Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| (Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN) >> (fn (imports, keywords) => make (name, pos) imports keywords)); end; (* read header *) val heading = (Parse.command_name chapterN || Parse.command_name sectionN || Parse.command_name subsectionN || Parse.command_name subsubsectionN || Parse.command_name paragraphN || Parse.command_name subparagraphN || Parse.command_name textN || Parse.command_name txtN || Parse.command_name text_rawN) -- (Document_Source.annotation |-- Parse.!!! Parse.document_source); val parse_header = (Scan.repeat heading -- Parse.command_name theoryN --| Document_Source.annotation) |-- Parse.!!! args; fun read_tokens pos toks = filter Token.is_proper toks |> Source.of_list |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! parse_header))) |> Source.get_single |> (fn SOME (header, _) => header | NONE => error ("Unexpected end of input" ^ Position.here pos)); local fun read_header pos text = Symbol_Pos.explode (text, pos) |> Token.tokenize bootstrap_keywords {strict = false} |> read_tokens pos; val approx_length = 1024; in fun read pos text = if size text <= approx_length then read_header pos text else let val approx_text = String.substring (text, 0, approx_length) in if String.isSuffix "begin" approx_text then read_header pos text else (read_header pos approx_text handle ERROR _ => read_header pos text) end; end; end;