# HG changeset patch
# User wenzelm
# Date 1606569927 -3600
# Node ID 1456c5747416808422cd08fdbf15a8d4797512b9
# Parent  e8da2cfdfcff13630348a348c0efcbe3b3e83d5d
clarified modules;

diff -r e8da2cfdfcff -r 1456c5747416 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sat Nov 28 14:25:27 2020 +0100
@@ -94,13 +94,13 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>spark_open_vcg\<close>
     "open a new SPARK environment and load a SPARK-generated .vcg file"
-    (Resources.provide_parse_files (Resources.extensions ["vcg", "fdl", "rls"]) -- Parse.parname
+    (Resources.provide_parse_files (Command_Span.extensions ["vcg", "fdl", "rls"]) -- Parse.parname
       >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>spark_open\<close>
     "open a new SPARK environment and load a SPARK-generated .siv file"
-    (Resources.provide_parse_files (Resources.extensions ["siv", "fdl", "rls"]) -- Parse.parname
+    (Resources.provide_parse_files (Command_Span.extensions ["siv", "fdl", "rls"]) -- Parse.parname
       >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
 
 val pfun_type = Scan.option
diff -r e8da2cfdfcff -r 1456c5747416 src/Pure/PIDE/command_span.ML
--- a/src/Pure/PIDE/command_span.ML	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/Pure/PIDE/command_span.ML	Sat Nov 28 14:25:27 2020 +0100
@@ -6,6 +6,7 @@
 
 signature COMMAND_SPAN =
 sig
+  val extensions: string list -> Path.T -> Path.T list
   datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
   datatype span = Span of kind * Token.T list
   val kind: span -> kind
@@ -18,6 +19,13 @@
 structure Command_Span: COMMAND_SPAN =
 struct
 
+(* loaded files *)
+
+fun extensions exts path = map (fn ext => Path.ext ext path) exts;
+
+
+(* span *)
+
 datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
 datatype span = Span of kind * Token.T list;
 
@@ -25,6 +33,9 @@
 fun content (Span (_, toks)) = toks;
 val symbol_length = Position.distance_of o Token.range_of o content;
 
+
+(* presentation positions *)
+
 fun adjust_offsets_kind adjust k =
   (case k of
     Command_Span (name, pos) => Command_Span (name, Position.adjust_offsets adjust pos)
diff -r e8da2cfdfcff -r 1456c5747416 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Nov 28 14:25:27 2020 +0100
@@ -37,7 +37,6 @@
   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 extensions: string list -> Path.T -> Path.T list
   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
@@ -293,8 +292,6 @@
 
 (* load files *)
 
-fun extensions exts path = map (fn ext => Path.ext ext path) exts;
-
 fun parse_files make_paths =
   Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
     (case Token.get_files tok of