16 |
16 |
17 type Loaded_Files = (List[String], Int) |
17 type Loaded_Files = (List[String], Int) |
18 |
18 |
19 val no_loaded_files: Loaded_Files = (Nil, -1) |
19 val no_loaded_files: Loaded_Files = (Nil, -1) |
20 |
20 |
21 def loaded_files(exts: List[String], tokens: List[(Token, Int)]): Loaded_Files = |
21 class Load_Command(val name: String) extends Isabelle_System.Service |
22 tokens.collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) match { |
22 { |
23 case Some((file, i)) => |
23 override def toString: String = name |
24 if (exts.isEmpty) (List(file), i) |
24 |
25 else (exts.map(ext => file + "." + ext), i) |
25 def extensions: List[String] = Nil |
26 case None => no_loaded_files |
26 |
27 } |
27 def loaded_files(tokens: List[(Token, Int)]): Loaded_Files = |
|
28 tokens.collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) match { |
|
29 case Some((file, i)) => |
|
30 extensions match { |
|
31 case Nil => (List(file), i) |
|
32 case exts => (exts.map(ext => file + "." + ext), i) |
|
33 } |
|
34 case None => no_loaded_files |
|
35 } |
|
36 } |
|
37 |
|
38 lazy val load_commands: List[Load_Command] = |
|
39 new Load_Command("") :: Isabelle_System.make_services(classOf[Load_Command]) |
28 |
40 |
29 |
41 |
30 /* span kind */ |
42 /* span kind */ |
31 |
43 |
32 sealed abstract class Kind { |
44 sealed abstract class Kind { |
105 else Nil |
117 else Nil |
106 } |
118 } |
107 |
119 |
108 def loaded_files(syntax: Outer_Syntax): Loaded_Files = |
120 def loaded_files(syntax: Outer_Syntax): Loaded_Files = |
109 syntax.load_command(name) match { |
121 syntax.load_command(name) match { |
110 case Some(exts) => isabelle.Command_Span.loaded_files(exts, clean_arguments) |
|
111 case None => no_loaded_files |
122 case None => no_loaded_files |
|
123 case Some(a) => |
|
124 load_commands.find(_.name == a) match { |
|
125 case Some(load_command) => load_command.loaded_files(clean_arguments) |
|
126 case None => error("Undefined load command function: " + a) |
|
127 } |
112 } |
128 } |
113 } |
129 } |
114 |
130 |
115 val empty: Span = Span(Ignored_Span, Nil) |
131 val empty: Span = Span(Ignored_Span, Nil) |
116 |
132 |